CONCUR 2000 — Concurrency Theory

Automated verification of concurrent systems is hindered by the fact that the state spaces are either infinite or too large for model checking, and the case analysis usually defeats theorem proving. Combinations of the two techniques have been tried with varying degrees of success. We argue for a specific combination where theorem proving is used to reduce verification problems to finite-state form, and model checking is used to explore properties of these reductions. This decomposition of the verification task forms the basis of the Symbolic Analysis Laboratory (SAL), a framework for combining different analysis tools for transition systems via a common intermediate language. We demonstrate how symbolic analysis can be an effective methodology for combining deduction and exploration.

The formal verification of concurrent systems is usually seen as an example par excellence of the application of mathematical methods to computer science. Although the practical application of such verification methods will always be limited by the underlying forms of combinatorial explosion, recent years have shown remarkable progress in computer aided formal verification. They are making formal verification a practical proposition for a growing class of real-life applications, and have put formal methods on the agenda of industry, in particular in the areas where correctness is critical in one sense or another. Paradoxically, the results of this progress provide evidence that successful applications of formal verification have significant elements that do not fit the paradigm of pure mathematical reasoning. In this essay we argue that verification is part of an experimental paradigm in at least two senses. We submit that this observation has consequences for the ways in which we should research and apply formal methods.

In this talk, I give an overview of some recent work, by my colleagues and me at Stony Brook, concerning compositional specification and performance analysis techniques for finite-state reactive systems in which probability and timing play a significant role.

Concurrency is an essential element of abstract models for embedded systems. Correctness and efficiency of the design depend critically on the way concurrency is formalized and implemented. Concurrency is about communicating processes. We introduce an abstract formal way of representing communication among processes and we show how to refine this representation towards implementation. To this end, we present a formal model, Abstract Co-design Finite State Machines (ACFSM), and its refinement, Extended Co-design Finite State Machines (ECFSM), developed to capture abstract behavior of concurrent processes and derived from a model (Co-design Finite State Machine (CFSM)) we have used in POLIS, a system for the design and verification of embedded systems. The design of communication protocols is presented as an example of the use of these formal models.

In the design of programming languages for highly distributed systems where processes can migrate and execute on new hosts, the integration of security mechanisms is a major challenge. In this paper, we report our experience in the design of an experimental programming language, called Klaim, which provides mechanisms to customize access control policies. Klaim security architecture exploits a capability-based type system to provide mechanisms for specifying and enforcing policies that control uses of resources and authorize migration and execution of processes. By means of a few programming examples, we illustrate the flexibility of the Klaim approach to support the specification of control policies and to guarantee their enforcement.

Model checking is emerging as a practical tool for automated debugging of reactive systems such as embedded controllers and network protocols [9,11]. Since model checking is based on exhaustive state-space exploration, and the size of the state space of a design grows exponentially with the size of the description, scalability remains a challenge. The goal of our recent research has been to develop techniques for exploiting the modular design structure during model checking. Software design notations (e.g. Statecharts [10], Uml) provide rich constructs to facilitate modular descriptions. Instead of destroying this structure by compiling the descriptions into flat state-transition graphs, we are developing algorithms that are optimized for modular descriptions. In this talk, we summarize research concerning two different notions of hierarchy: architectural and behavioral.

We present two process frameworks: the action calculi of Milner, and the fusion systems of Gardner and Wischik. The action calculus framework is based on process constructs arising from the π-calculus. We give a non-standard presentation of the π-calculus, to emphasise the similarities between the calculus and the framework. The fusion system framework generalises a new process calculus called the π_F-calculus. We describe the π_F-calculus, which is based on different process constructs to those of the π-calculus, and show that the generalisation from the calculus to the framework is simple. We compare the frameworks by studying examples.

The LMC project aims to advance the state of the art of system specification and verification using the latest developments in logic programming technology [CDD+98]. Initially, the project was focussed on developing an efficient model checker, called XMC [RRR+97], for value-passing CCS [Mil89] and the modal mu-calculus [Koz83] based on the XSB logic programming system [XSB00]. We developed an optimizing compiler to translate specifications in a dialect of value-passing CCS to compact labeled transition systems [DR99], improving verification performance several fold. The core principles of this translation have been recently incorporated in SPIN [Hol97] showing similar gains in performance [Hol99]. The XMC system can be downloaded from http://www.cs.sunysb.edu/~lmc.More recently, we have developed techniques using logic-program transformations [TS84,PP99,RKRR99] for verifying parameterized systems, i.e., infinite families of finite-state systems [RKR+00];a proof-tree viewer for justifying successful or failed verification runs for branching-time properties [RRR00];a symbolic bisimulation checker (based on the work of [HL95]) for value-passing systems [MRRV00];model checkers for real-time systems [DRS00] based loosely on the local model checking algorithm of [SS95];LTL with actions [PR00] based on GCTL* of [BCG00] and the on-the-fly model checking algorithm in [BCG95];In this tutorial, we describe the XMC system as well as the above developments. In addition, we outline the research efforts of the verification and the logic programming community that have been instrumental in these developments.

We study the problems of synthesizing open systems as well as controllers for them. The key aspect of our model is that it caters to reactive environments, which can disable different sets of responses when reacting with the system. We deal with specifications given as formulas in CTL* and its sub-logic CTL. We show that both these problems, with specifications in CTL (CTL*), are 2EXPTIME-complete (resp. 3EXPTIME-complete). Thus, in a sense, reactive environments constitute a provably harder setting for the synthesis of open systems and controllers for them.

Unfoldings are a technique for verification of concurrent and distributed systems introduced by McMillan. The method constructs a finite complete prefix, which can be seen as a symbolic representation of an interleaved reachability graph. We show that model checking a fixed size formula of several temporal logics, including LTL, CTL, and CTL*, is PSPACE-complete in the size of a finite complete prefix of a 1-safe Petri net. This proof employs a class of 1-safe Petri nets for which it is easy to generate a finite complete prefix in polynomial time.

We consider the problem of automatically verifying realtime systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in [19], an extension of the timed automata model of [4], with clock resets made according to continuous probability distributions. Thus, our model exhibits nondeterministic and probabilistic choice, the latter being made according to both discrete and continuous probability distributions. To facilitate algorithmic verification, we modify the standard region graph construction by subdividing the unit intervals in order to approximate the probability to within an interval. We then develop a model checking method for continuous probabilistic timed automata, taking as our specification language Probabilistic Timed Computation Tree Logic (PTCTL). Our method improves on the previously known techniques in that it allows the verification of quantitative probability bounds, as opposed to qualitative properties which can only refer to bounds of probability 0 or 1.

In this paper we define and study the class of stopwatch automata which are timed automata augmented with stopwatches and unobservable behaviour. In particular, we investigate the expressive power of this class of automata, and show as a main result that any finite or infinite timed language accepted by a linear hybrid automaton is also acceptable by a stopwatch automaton. The consequences of this result are two-fold: firstly, it shows that the seemingly minor upgrade from timed automata to stopwatch automata immediately yields the full expressive power of linear hybrid automata. Secondly, reachability analysis of linear hybrid automata may effectively be reduced to reachability analysis of stopwatch automata. This, in turn, may be carried out using an easy (over-approximating) extension of the efficient reachability analysis for timed automata to stopwatch automata. We report on preliminary experiments on analyzing translations of linear hybrid automata using a stopwatch-extension of the real-time verification tool UPPAAL.

We describe a family of optimizations implemented in a translation from a linear temporal logic to Büchi automata. Such optimized automata can enhance the efficiency of model checking, as practiced in tools such as Spin. Some of our optimizations are applied during preprocessing of temporal formulas, while other key optimizations are applied directly to the resulting Büchi automata independent of how they arose. Among these latter optimizations we apply a variant of fair simulation reduction based on color refinement. We have implemented our optimizations in a translation of an extension to LTL described in [Ete99]. Inspired by this work, a subset of the optimizations outlined here has been added to a recent version of Spin. Both implementations begin with an underlying algorithm of [GPVW95]. We describe the results of tests we have conducted, both to see how the optimizations improve the sizes of resulting automata, as well as to see how the smaller sizes for the automata affect the running time of Spin’s explicit state model checking algorithm. Our translation is available via a web-server which includes a GUI that depicts the resulting automata: http://cm.bell-labs.com/cm/cs/what/spin/eqltl.html

We discuss the problem of model checking temporal properties on partial Kripke structures, which were used in [BG99] to represent incomplete state spaces. We first extend the results of [BG99] by showing that the model-checking problem for any 3-valued temporal logic can be reduced to two model-checking problems for the corresponding 2-valued temporal logic. We then introduce a new semantics for 3-valued temporal logics that can give more definite answers than the previous one. With this semantics, the evaluation of a formula φ on a partial Kripke structure M returns the third truth value ⊥ (read “unknown”) only if there exist Kripke structures M₁ and M₂ that both complete M and such that M₁ satisfies φ while M₂ violates φ, hence making the value of φ on M truly unknown. The partial Kripke structure M can thus be viewed as a partial solution to the satisfiability problem which reduces the solution space to complete Kripke structures that are more complete than M with respect to a completeness preorder. This generalized model-checking problem is thus a generalization of both satisfiability (all Kripke structures are potential solutions) and model checking (a single Kripke structure needs to be checked). We present algorithms and complexity bounds for the generalized model-checking problem for various temporal logics.

We introduce some new models of infinite-state transition systems. The basic model, called a (reversal-bounded) counter machine (CM), is a nondeterministic finite automaton augmented with finitely many reversal-bounded counters (i.e. each counter can be incremented or decremented by 1 and tested for zero, but the number of times it can change mode from nondecreasing to nonincreasing and vice-versa is bounded by a constant, independent of the computation). We extend a CM by augmenting it with some familiar data structures: (i) A pushdown counter machine (PCM) is a CM augmented with an unrestricted pushdown stack. (ii) A tape counter machine (TCM) is a CM augmented with a two-way read/write worktape that is restricted in that the number of times the head crosses the boundary between any two adjacent cells of the worktape is bounded by a constant, independent of the computation (thus, the worktape is finite-crossing). There is no bound on how long the head can remain on a cell. (iii) A queue counter machine (QCM) is a CM augmented with a queue that is restricted in that the number of alternations between non-deletion phase and non-insertion phase is bounded by a constant. A non-deletion (non-insertion) phase is a period consisting of insertions (deletions) and no-changes, i.e., the queue is idle. We show that emptiness, (binary, forward, and backward) reachability, nonsafety, and invariance for these machines are solvable. We also look at extensions of the models that allow the use of linear-relation tests among the counters and parameterized constants as “primitive” predicates. We investigate the conditions under which these problems are still solvable.

This paper presents process spaces, a general theory for systems that are made of several interacting components and layers of abstraction. Process spaces capture in a homogeneous manner diverse correctness concerns for concurrent systems and other types of systems. The main innovation of process spaces is the idea of abstract execution, which permits to set the precision and complexity of a system model by the amount of detail included in the execution model. Notwithstanding this generality, we show that process spaces admit several algebraic properties of practical significance.

In this paper, we present a semantic theory for the exchange of information in multi-agent systems. We define a concurrent programming language for systems of agents that maintain their own private stores of information and that interact with each other by means of a synchronous communication mechanism that allows for the exchange of information. The semantics of the language, which is based on a generalisation of traditional failure semantics, is shown to be fully-abstract with respect to observing of each terminating computation its final global store of information.

We introduce an assertional method for specifying and proving properties of the multi-threaded flow of control in Java. The method integrates in a modular manner reasoning about the shared-variable concurrency within one object and the communication of values between threads.

The dynamics of reactive systems, e.g. CCS, has often been defined using a labelled transition system (LTS). More recently it has become natural in defining dynamics to use reaction rules - i.e. unlabelled transition rules - together with a structural congruence. But LTSs lead more naturally to behavioural equivalences. So one would like to derive from reaction rules a suitable LTS.This paper shows how to derive an LTS for a wide range of reactive systems. A label for an agent a is defined to be any context F which intuitively is just large enough so that the agent Fa (“a in context F”) is able to perform a reaction. The key contribution of this paper is a precise definition of “just large enough”, in terms of the categorical notion of relative pushout (RPO), which ensures that bisimilarity is a congruence when sufficient RPOs exist. Two examples - a simplified form of action calculi and term-rewriting - are given, for which it is shown that sufficient RPOs indeed exist. The thrust of this paper is, therefore, towards a general method for achieving useful behavioural congruence relations.

The definition of sos formats ensuring that bisimilarity on closed terms is a congruence has received much attention in the last two decades. For dealing with open terms, the congruence is usually lifted from closed terms by instantiating the free variables in all possible ways; the only alternatives considered in the literature are Larsen and Xinxin’s context systems and Rensink’s conditional transition systems. We propose an approach based on tile logic, where closed and open terms are managed uniformly, and study the ‘bisimilarity as congruence’ property for several tile formats, accomplishing different concepts of open system.

We present a general class of process languages for rooted eager bisimulation preorder and prove its congruence result. Also, we present classes of process languages for the rooted versions of several other weak preorders. The process languages we propose are defined by the Ordered SOS method which combines the traditional SOS approach, based on transition rules, with the ordering on transition rules. This new feature specifies the order of application of rules when deriving transitions of process terms. We support and illustrate our results with examples of process operators and process languages which benefit from the OSOS formulation.

The question we consider in this paper is: “When can a combination of fine-grain execution steps be contracted into an atomic action execution”? Our answer is basically: “When no observer can see the difference.” This is worked out in detail by defining a notion of coupled split/atomic simulation refinement between systems which differ in the atomicity of their actions, and proving that this collapses to Parrow and Sjödin’s coupled similarity when the systems are composed with an observer.

We present a testing theory for Markovian processes in order to formalize a notion of efficiency which may be useful for the analysis of soft real time systems. Our Markovian testing theory is shown to enjoy close connections with the classical testing theory of De Nicola-Hennessy and the probabilistic testing theory of Cleaveland-Smolka et al. The Markovian testing equivalence is also shown to be coarser than the Markovian bisimulation equivalence. A fully abstract characterization is developed to ease the task of establishing testing related relationships between Markovian processes. It is then demonstrated that our Markovian testing equivalence, which is based on the (easier to work with) probability of executing a successful computation whose average duration is not greater than a given amount of time, coincides with the Markovian testing equivalence based on the (more intuitive) probability of reaching success within a given amount of time. Finally, it is shown that it is not possible to define a Markovian preorder which is consistent with reward based performance measures, thus justifying why a generic notion of efficiency has been considered.

We consider the problem of deciding whether an infinite-state system (expressed as a Markov chain) satisfies a correctness property with probability 1. This problem is, of course, undecidable for general infinite-state systems. We focus our attention on the model of probabilistic lossy channel systems consisting of finite-state processes that communicating over unbounded lossy FIFO channels. Abdulla and Jonsson have shown that safety properties are decidable while progress properties are not for non-probabilistic lossy channel systems. Under assumptions of “sufficiently high” probability of loss, Baier and Engelen have shown how to check whether a property holds of probabilistic lossy channel system with probability 1.In this paper we show that the problem of checking whether a progress property holds with probability 1 is undecidable, if the assumption about “sufficiently high” probability of loss is omitted. More surprisingly, we show that checking whether safety properties hold with probability 1 is undecidable too. Our proof depends upon simulating a perfect channel, with a high degree of confidence, using lossy channels.

In this paper, we introduce weak bisimulation in the framework of Labeled Concurrent Markov Chains, that is, probabilistic transition systems which exhibit both probabilistic and nondeterministic behavior. By resolving the nondeterminism present, these models can be decomposed into a possibly infinite number of computation trees. We show that in order to compute weak bisimulation it is sufficient to restrict attention to only a finite number of these computations. Finally, we present an algorithm for deciding weak bisimulation which has polynomial-time complexity in the number of states of the transition system.

In this paper we describe how to build semantic models that support both nondeterministic choice and probabilistic choice. Several models exist that support both of these constructs, but none that we know of satisfies all the laws one would like. Using domain-theoretic techniques, we show how models can be devised using the “standard model” for probabilistic choice, and then applying modified domain-theoretic models for nondeterministic choice. These models are distinguished by the fact that the expected laws for nondeterministic choice and probabilistic choice remain valid. We also describe a potential application of our model to aspects of security.

We add an operation of group creation to the typed π - calculus, where a group is a type for channels. Creation of fresh groups has the effect of statically preventing certain communications, and can block the accidental or malicious leakage of secrets. Intuitively, no channel belonging to a fresh group can be received by processes outside the initial scope of the group, even if those processes are untyped. We formalize this intuition by adapting a notion of secrecy introduced by Abadi, and proving a preservation of secrecy property.

We study the verification of secrecy and authenticity properties for cryptographic protocols which rely on symmetric shared keys. The verification can be reduced to check whether a certain parallel program which models the protocol and the specification can reach an erroneous state while interacting with an adversary. Assuming finite principals, we present a decision procedure for the reachability problem which is based on a ‘symbolic’ reduction system.

Information flow security is that aspect of computer security concerned with how confidential information is allowed to flow through a computer system. This is especially subtle when considering processes that are executed concurrently. We consider the notion of Probabilistic Noninterference (PNI) proposed in the literature to ensure secure information flow in concurrent processes. In the setting of a model of probabilistic dataflow, we provide a number of important results towards simplified verification that suggest relevance in the interaction of probabilistic processes outside this particular framework:PNI is shown to be compositional by casting it into a rely-guarantee framework, where the proof yields a more general Inductive Compositionality Principle. We deliver a considerably simplified criterion equivalent to PNI by “factoring out” the probabilistic behaviour of the environment. We show that the simpler nonprobabilistic notion of Nondeducibility-on-Strategies proposed in the literature is an instantiation of PNI, allowing us to extend our results to it.

Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state space explosion problem. One of the ways to exploit such a semantics is to consider (finite prefixes of) net unfoldings — themselves a class of acyclic Petri nets — which contain enough information, albeit implicit, to reason about the reachable markings of the original Petri nets. In [15], a verification technique for net unfoldings was proposed in which deadlock detection was reduced to a mixed integer linear programming problem. In this paper, we present a further development of this approach. We adopt Contejean-Devie’s algorithm for solving systems of linear constraints over the natural numbers domain and refine it, by taking advantage of the specific properties of systems of linear constraints to be solved. The essence of the proposed modifications is to transfer the information about causality and conflicts between the events involved in an unfolding, into a relationship between the corresponding integer variables in the system of linear constraints. Experimental results demonstrate that the new technique achieves significant speedups.

Mazurkiewicz traces can be seen as equivalence classes of words or as pomsets. Their generalisation by local traces was formalized by Hoogers, Kleijn and Thiagarajan as equivalence classes of step firing sequences. First we introduce a pomset representation for local traces. Extending Büchi’s Theorem and a previous generalisation to Mazurkiewicz traces, we show then that a local trace language is recognized by a finite step transition system if and only if its class of pomsets is bounded and definable in the Monadic Second Order logic. Finally, using Zielonka’s Theorem, we show that each recognizable local trace language is described by a finite safe labelled Petri net.The complete version [22] of this paper is accessible on the web.

We propose a functorial concurrent semantics for Petri nets extended with read and inhibitor arcs, that we call inhibitor nets. Along the lines of the seminal work of Winskel on safe nets, the truly concurrent semantics is given at a categorical level via a chain of functors leading from the category SW-IN of semi-weighted inhibitor nets to the category Dom of finitary prime algebraic domains. As an intermediate semantic model, we introduce inhibitor event structures, an extension of prime event structures able to faithfully capture the dependencies among events which arise in the presence of read and inhibitor arcs.

In the synchronous composition of processes, one process may prevent another process from proceeding unless compositions without a well-defined product behavior are ruled out. They can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping processes with types, which make the dependencies between input and output signals transparent. We classify various typing mechanisms and study their effects on the control problem.A static type enforces fixed, acyclic dependencies between input and output ports. For example, synchronous hardware without combinational loops can be typed statically. A dynamic type may vary the dependencies from state to state, while maintaining acyclicity, as in level-sensitive latches. Then, two dynamically typed processes can be syntactically compatible, if all pairs of possible dependencies are compatible, or semantically compatible, if in each state the combined dependencies remain acyclic. For a given plant process and control objective, there may be a controller of a static type, or only a controller of a syntactically compatible dynamic type, or only a controller of a semantically compatible dynamic type. We show this to be a strict hierarchy of possibilities, and we present algorithms and determine the complexity of the corresponding control problems.Furthermore, we consider versions of the control problem in which the type of the controller (static or dynamic) is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions.

Concurrent objects may offer services non-uniformly, constraining the acceptance of messages on the states of objects. We advocate a looser view of communication errors. Safe programmes must guarantee that every message has a chance of being received if it requests a method that may become enabled at some point in the future. We formalise non-uniform concurrent objects in T_yCO, a name-passing object calculus, and ensure program safety via a type system. Types are terms of a process algebra that describes dynamic aspects of the behaviour of objects.

We extend Kobayashi and Sumii’s type system for the deadlock-free π-calculus and develop a type reconstruction algorithm. Kobayashi and Sumii’s type system helps high-level reasoning about concurrent programs by guaranteeing that communication on certain channels will eventually succeed. It can ensure, for example, that a process implementing a function really behaves like a function. However, because it lacked a type reconstruction algorithm and required rather complicated type annotations, applying it to real concurrent languages was impractical. We have therefore developed a type reconstruction algorithm for an extension of the type system. The key novelties that made it possible are generalization of usages (which specifies how each communication channel is used) and a subusage relation.

We describe a general model for embedding object-oriented constructs into calculi of mobile agents. The model results from extending agents with methods and primitives for message passing. We then study an instance of the model based on Cardelli and Gordon’s Mobile Ambients. We define a type system for the resulting calculus, give a subject reduction theorem, and discuss the rôle of the type system for static detection of run-time type errors and for other program verification purposes.

Message sequence charts (MSCs) are an appealing visual formalism often used to capture system requirements in the early stages of design. An important question concerning MSCs is the following: how does one convert requirements represented by MSCs into state-based specifications? A first step in this direction was the definition in [9] of regular collections of MSCs, together with a characterization of this class in terms of finite-state distributed devices called message-passing automata. These automata are, in general, nondeterministic. In this paper, we strengthen this connection and describe how to directly associate a deterministic message-passing automaton with each regular collection of MSCs. Since real life distributed protocols are deterministic, our result is a more comprehensive solution to the synthesis problem for MSCs. Our result can be viewed as an extension of Zielonka’s theorem for Mazurkiewicz trace languages [6,19] to the setting of finite-state message-passing systems.

We resume the investigation of asynchronous cellular automata. Originally, these devices were considered in the context of Mazurkiewicz traces, and later generalized to run on arbitrary pomsets without autoconcurrency by Droste and Gastin [3]. While the universality of the accepted language is known to be undecidable [11], we show here that the emptiness is decidable. Our proof relies on a result due to Finkel and Schnoebelen [7] on well-structured transition systems.

Safety and liveness are two fundamental concepts for proving the correctness of concurrent programs. In the context of failures, however, we observe that some properties that are commonly believed to be safety properties are actually liveness properties. In this paper, we propose refinements of the concepts of safety and liveness that avoid this counterintuitive classification.

Formal methods based on symbolic representations have been found to be very effective. In the case of infinite state systems, there has been a great deal of interest in accelerations - a technique for characterizing the result of iterating an execution sequence an arbitrary number of times, in a sound, but not necessarily complete, way. We propose the use of abstractions as a general framework to design accelerations. We investigate SemiLinear Regular Expressions (SLREs) as symbolic representations for FIFO automata. In particular, we show that SLREs are easy to manipulate (inclusion between two SLREs is in NP∩coNP), they form the core of known FIFO symbolic representations (SLREs = QDDs∩CQDDs), and they are usually sufficient since for FIFO automata with one channel, an arbitrary iteration of a loop is LRE representable.

A concurrent system is data-independent with respect to a data type when the only operation it can perform on values of that type is equality testing. The system can also assign, input, nondeterministically choose, and output such values. Based on this intuitive definition, syntactic restrictions which ensure data-independence have been formulated for a variety of different formalisms. However, it is difficult to see how these are related.We present the first semantic definition of data-independence which allows equality testing, and its extension which allows constant symbols and predicate symbols. Both are special cases of a definition of when a family of labelled transition systems is parametric. This provides a unified approach to data-independence and its extensions.The paper also contains two theorems which, given a system and a specification which are data-independent, enable the verification for all instantiations of the data types (and of the constant symbols and the predicate symbols, in the case of the extension) to be reduced to the verification for a finite number of finite instantiations.We illustrate the applicability of the approach to particular formalisms by a programming language similar to UNITY.

The theory of chi processes with the mismatch operator is studied. Two open congruence relations are investigated. These are weak early open congruence and weaklate open congruence. Complete systems are given for both congruence relations. These systems use some new tau laws. The results of this paper correct some popular mistakes in literature.