Towards a theory of bisimulation for the higher-order process calculi

In this paper, a labelled transition semantics for higher-order process calculi is studied. The labelled transition semantics is relatively clean and simple, and corresponding bisimulation equivalence can be easily formulated based on it. And the congruence properties of the bisimulation equivalence can be proved easily. To show the correspondence between the proposed semantics and the well-established ones, the bisimulation is characterized as a version of barbed equivalence and a version of context bisimulation.     

Computable processes and bisimulation equivalence

A process is calledcomputable if it can be modelled by a transition system that has a recursive structure—implying finite branching. The equivalence relation between transition systems considered is strong bisimulation equivalence. The transition systems studied in this paper can be associated to processes specified in common specification languages such as CCS, LOTOS, ACP and PSF. As a means for defining transition systems up to bisimulation equivalence, the specification languageCRL is used. Two simple fragments of,CRL are singled out, yielding universal expressivity with respect to recursive and primitive recursive transition systems. For both these domains the following properties are classified in the arithmetical hierarchy:bisimilarity, perpetuity (both ₁ ⁰ ),regularity (having a bisimilar, finite representation, ₂ ⁰ ),acyclic regularity ( ₁ ⁰ ), anddeadlock freedom (distinguishing deadlock from successful termination, ₁ ⁰ ). Finally, it is shown that in the domain of primitive recursive transition systems over a fixed, finite label set, a genuine hierarchy in bisimilarity can be defined by the complexity of the witnessing relations, which extends r.e. bisimilarity. Hence, primitive recursive transition systems already form an interesting class.     

Deciding bisimulation and trace equivalences for systems with many identical processes

In the study of process semantics, trace equivalence and bisimulation equivalence constitute the two extremes of the so-called linear time—branching time spectrum. In this paper, we study the complexity and decidability issues of deciding trace and bisimulation equivalences for the model of systems with many identical processes with respect to various interprocess communication structures. In our model, each system consists of an arbitrary number of identical finite-state processes using Milner's calculus of communicating systems (CCS) as the style of interprocess communication. As it turns out, deciding trace and bisimulation equivalences are undecidable for star-like and linear systems, whereas the two problems are complete for PSPACE and PTIME, respectively, for fully connected systems.     

Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes

In a recent paper Baier et al. [Lecture Notes in Computer Science, Springer-Verlag, 2000, p. 358] analyzed a new way of model-checking formulas of a logic for continuous-time processes—called continuous stochastic logic (henceforth CSL)—against continuous-time Markov chains—henceforth CTMCs. One of the important results of that paper was the proof that if two CTMCs were bisimilar then they would satisfy exactly the same formulas of CSL. This raises the converse question—does satisfaction of the same collection of CSL formulas imply bisimilarity? In other words, given two CTMCs which are known to satisfy exactly the same formulas of CSL does it have to be the case that they are bisimilar? We prove that the answer to the question just raised is “yes”. In fact we prove a significant extension, namely that a subset of CSL suffices even for systems where the state space may be a continuum. Along the way we prove a result to the effect that the set of Zeno paths has measure zero provided that the transition rates are bounded.     

生成诊断公式的有限状态进程等价验证

分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题.给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统.给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式.算法的时间复杂度为O(m log n),空间复杂度为O(m+n).     

On parameterization of higher-order processes

Parameterization provides an effective way to improve on the expressiveness of process-passing. In this paper, we study two kinds of parameterization: name parameterization and process parameterization. Firstly, we show that process parameterization retains the characterization of context bisimulation in terms of the far simpler normal bisimulation, in which universal quantifiers are eliminated. Secondly, we prove that name parameterization is at least as expressive as process parameterization by giving an encoding from the higher-order calculus with process parameterization into the higher-order calculus with name parameterization. These results clarify further the theoretical framework of higher-order processes, and shed light on the relationship between the two kinds of parameterization.     

Weak bisimulation for Probabilistic Timed Automata

We are interested in describing timed systems that exhibit probabilistic behaviour. To this purpose, we consider a model of Probabilistic Timed Automata and introduce a concept of weak bisimulation for these automata, together with an algorithm to decide it. The weak bisimulation relation is shown to be preserved when either time, or probability is abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.     

Branching bisimulation congruence for probabilistic systems

A notion of branching bisimilarity for the alternating model of probabilistic systems, compatible with parallel composition, is defined. For a congruence result, an internal transition immediately followed by a non-trivial probability distribution is not considered inert. A weaker definition of branching bisimilarity for the same model has been given earlier. Here we show that our branching bisimulation is the coarsest congruence for parallel composition that is included in the weaker version. To support the use of the present equivalence as a reduction technique, we also show that probabilistic CTL formulae are preserved by our equivalence, and we provide a polynomial-time algorithm deciding branching bisimilarity.     

Linearity and bisimulation

Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the π-calculus in which we abstract away not only τ-actions but also non-τ actions which do not affect well-typed observers. This gives a congruence far larger than the standard bisimilarity while retaining semantic soundness. The framework is smoothly extendible to other settings involving nondeterminism and state. As an application we develop a behavioural theory of secrecy in the π-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach, while still offering compositional verification techniques.     

Deciding orthogonal bisimulation

Bergstra, Ponse and van der Zwaag introduced in 2003 the notion of orthogonal bisimulation equivalence on labeled transition systems. This equivalence is a refinement of branching bisimulation, in which consecutive tau’s (silent steps) can be compressed into one (but not zero) tau’s. The main advantage of orthogonal bisimulation is that it combines well with priorities. Here we solve the problem of deciding orthogonal bisimulation equivalence in finite (regular) labeled transition systems. Unlike as in branching bisimulation, in orthogonal bisimulation, cycles of silent steps cannot be eliminated. Hence, the algorithm of Groote and Vaandrager (1990) cannot be adapted easily. However, we show that it is still possible to decide orthogonal bisimulation with the same complexity as that of Groote and Vaandrager’s algorithm. Thus if n is the number of states, and m the number of transitions then it takes O(n(m + n)) time to decide orthogonal bisimilarity on finite labeled transition systems, using O(m + n) space. J. Parrow     

Approximate bisimulation relations for constrained linear systems

In this paper, we define the notion of approximate bisimulation relation between two continuous systems. While exact bisimulation requires that the observations of two systems are and remain identical, approximate bisimulation allows the observations to be different provided the distance between them remains bounded by some parameter called precision. Approximate bisimulation relations are conveniently defined as level sets of a so-called bisimulation function which can be characterized using Lyapunov-like differential inequalities. For a class of constrained linear systems, we develop computationally effective characterizations of bisimulation functions that can be interpreted in terms of linear matrix inequalities and optimal values of static games. We derive a method to evaluate the precision of the approximate bisimulation relation between a constrained linear system and its projection. This method has been implemented in a Matlab toolbox: MATISSE. An example of use of the toolbox in the context of safety verification is shown.     

Multi-core symbolic bisimulation minimisation

We introduce parallel symbolic algorithms for bisimulation minimisation, to combat the combinatorial state space explosion along three different paths. Bisimulation minimisation reduces a transition system to the smallest system with equivalent behaviour. We consider strong and branching bisimilarity for interactive Markov chains, which combine labelled transition systems and continuous-time Markov chains. Large state spaces can be represented concisely by symbolic techniques, based on binary decision diagrams. We present specialised BDD operations to compute the maximal bisimulation using signature-based partition refinement. We also study the symbolic representation of the quotient system and suggest an encoding based on representative states, rather than block numbers. Our implementation extends the parallel, shared memory, BDD library Sylvan, to obtain a significant speedup on multi-core machines. We propose the usage of partial signatures and of disjunctively partitioned transition relations, to increase the parallelisation opportunities. Also our new parallel data structure for block assignments increases scalability. We provide SigrefMC, a versatile tool that can be customised for bisimulation minimisation in various contexts. In particular, it supports models generated by the high-performance model checker LTSmin, providing access to specifications in multiple formalisms, including process algebra. The extensive experimental evaluation is based on various benchmarks from the literature. We demonstrate a speedup up to 95\(\times \) for computing the maximal bisimulation on one processor. In addition, we find parallel speedups on a 48-core machine of another 17\(\times \) for partition refinement and 24\(\times \) for quotient computation. Our new encoding of the reduced state space leads to smaller BDD representations, with up to a 5162-fold reduction.

     

Open bisimulation,revisited

In the context of the π$\pi$-calculus, open bisimulation is prominent and popular due to its congruence properties and its easy implementability. Motivated by the attempt to generalise it to the spi-calculus, we offer a new, more refined definition and show how far it coincides with the original one.     

A theory of bisimulation for the π-calculus

 We study a new formulation of bisimulation for the π-calculus [MPW92], which we have called open bisimulation (∼). In contrast with the previously known bisimilarity equivalences, ∼ is preserved by allπ-calculus operators, including input prefix. The differences among all these equivalences already appear in the sublanguage without name restrictions: Here the definition of ∼ can be factorised into a “standard” part which, modulo the different syntax of actions, is the CCS bisimulation, and a part specific to the π-calculus, which requires name instantiation. Attractive features of ∼ are: A simple axiomatisation (of the finite terms), with a completeness proof which leads to the construction of minimal canonical representatives for the equivalence classes of ∼; an “efficient” characterisation, based on a modified transition system. This characterisation seems promising for the development of automated-verification tools and also shows the call-by-need flavour of ∼. Although in the paper we stick to the π-calculus, the issues developed may be relevant to value-passing calculi in general. Received: June 11, 1993/November 28, 1994     

Control of nondeterministic discrete-event systems for bisimulation equivalence

Most prior work on supervisory control of discrete event systems is for achieving deterministic specifications, expressed as formal languages. In this paper we study supervisory control for achieving nondeterministic specifications. Such specifications are useful when designing a system at a higher level of abstraction so that lower level details of system and its specification are omitted to obtain higher level models that may be nondeterministic. Nondeterministic specifications are also meaningful when the system to be controlled has a nondeterministic model due to the lack of information (caused for example by partial observation or unmodeled dynamics). Language equivalence is not an adequate notion of behavioral equivalence for nondeterministic systems, and instead we use the finest known notion of equivalence, namely the bisimulation equivalence. Choice of bisimulation equivalence is also supported by the fact that bisimulation equivalence specification is equivalent to a specification in the temporal logic of /spl mu/-calculus that subsumes the complete branching-time logic CTL*. Given nondeterministic models of system and its specification, we study the design of a supervisor (possibly nondeterministic) such that the controlled system is bisimilar to the specification. We obtain a small model theorem showing that a supervisor exists if and only if it exists over a certain finite state space, namely the power set of Cartesian product of system and specification state spaces. Also, the notion of state-controllability is introduced as part of a necessary and sufficient condition for the existence of a supervisor. In the special case of deterministic systems, we provide an existence condition that can be verified polynomially in both system and specification states, when the existence condition holds.     

Approximating bisimulation in one-counter nets

One-counter nets are finite-state machines operating on a variable (counter), which ranges over the natural numbers. Each transition can increase or decrease the counter’s value, and a decrease is possible only if the result is nonnegative; hence, zero testing is not allowed. The class of one-counter nets is equivalent in terms of its expressive power to the class of Petri nets with one unbounded place and to the class of pushdown automata where the stack alphabet contains one symbol. We present a specific method of approximating the largest bisimulation of a one-counter net based on single-periodic arithmetic and the notion of stratified bisimulation.     

Distinguishing and relating higher-order and first-order processes by expressiveness

This is a paper on distinguishing and relating two important kinds of calculi through expressiveness, settling some critical but long unanswered questions. The delimitation of higher-order and first-order process calculi is a basic and pivotal topic in the study of process theory. Particularly, expressiveness studies mutual encodability, which helps decide whether process-passing or name-passing is more fundamental, and the way they ought to be used in both theory and practice. In this paper, we contribute to such demarcation with three major results. Firstly $\pi $ (first-order pi-calculus) can faithfully express $\varPi $ (basic higher-order pi-calculus). The calculus $\varPi $ has the elementary operators (input, output, composition and restriction). This actually is a corollary of a more general result, that $\pi $ can encode $\varPi ^r$ ( $\varPi $ enriched with the relabelling operator). Secondly $\varPi $ cannot interpret $\pi $ reasonably. This is of more significance since it separates $\varPi $ and $\pi $ by drawing a well-defined boundary. Thirdly an encoding from $\pi $ to $\varPi ^r$ is revisited and discussed, which not only implies how to make $\varPi $ more useful but also stresses the importance of name-passing in $\pi $ .     

Branching bisimulation for probabilistic systems: Characteristics and decidability

We address the concept of abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model of Hansson. In particular, we define the notion of branching bisimilarity and study its properties by studying two other equivalence relations, viz. coloured trace equivalence and branching bisimilarity using maximal probabilities. We show that both alternatives coincide with branching bisimilarity. The alternative characterisations have their own merits and focus on different aspects of branching bisimilarity. Coloured trace equivalence can be understood without knowledge of probability theory and is independent of the notion of a scheduler. Branching bisimilarity, rephrased in terms of maximal probabilities gives rise to an algorithm of polynomial complexity for deciding the equivalence. Together they give a better understanding of branching bisimilarity. Furthermore, we show that the notions of branching bisimilarity in the alternating model of Hansson and in the non-alternating model of Segala differ: branching bisimilarity in the latter setting turns out to discriminate between systems that are intuitively branching bisimilar.     

Controller synthesis for safety and reachability via approximate bisimulation

In this paper, we consider the problem of controller design using approximately bisimilar abstractions with an emphasis on safety and reachability specifications. We propose abstraction-based approaches to controller synthesis for both types of specifications. We start by synthesizing a controller for an approximately bisimilar abstraction. Then, using a concretization procedure, we obtain a controller for our initial system that is proved “correct by design”. We provide guarantees of performance by giving estimates of the distance of the synthesized controller to the maximal (i.e., the most permissive) safety controller or to the time-optimal reachability controller. Finally, we use these techniques, combined with discrete approximately bisimilar abstractions of switched systems developed recently, for switching controller synthesis.