From SOS Specifications to Structured Coalgebras: How to Make Bisimulation a Congruence

In this paper we address the issue of providing a structured coalgebra presentation of transition systems with algebraic structure on states determined by an equational specification Γ. More precisely, we aim at representing such systems as coalgebras for an endofunctor on the category of Γ-algebras. The systems we consider are specified by using a quite general format of SOS rules, the algebraic format, which in general does not guarantee that bisimilarity is a congruence.We first show that the structured coalgebra representation works only for systems where transitions out of complex states can be derived from transitions out of corresponding component states. This decomposition property of transitions indeed ensures that bisimilarity is a congruence. For a system not satisfying this requirement, next we propose a closure construction which adds context transitions, i.e., transitions that spontaneously embed a state into a bigger context or vice-versa. The notion of bisimulation for the enriched system coincides with the notion of dynamic bisimilarity for the original one, that is, with the coarsest bisimulation which is a congruence. This is sufficient to ensure that the structured coalgebra representation works for the systems obtained as result of the closure construction.     

A Syntactical Approach to Weak (Bi-)Simulation for Coalgebras

In [19] Rutten introduced the notion of weak bisimulations and weak bisimilarity for coalgebras of the functor F(X) = X + O. In the present paper I will introduce a notion of weak bisimulation for coalgebras based on the syntax of their functors for a large class of functors. I will show that my definition does not only coincide with the definition from [19], but with the definition for labelled transition systems as well. The approach includes a definition of weak bisimulation for Kripke structures, which might be of interest in its own right.     

Open Bisimulation, Revisited

In the context of the π-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 in how far it coincides with the original one.     

互模拟与逻辑

本文首先讨论了模态逻辑与μ算子的表达能力、博弈语义,给出一阶逻辑与Monadic二阶逻辑的博弈形式,然后讨论互模拟等价在这些逻辑表达能力的核心作用和这些逻辑之间的关系。     

Comprehension for Coalgebras

The notion of an endofunctor having “greatest subcoalgebras” is introduced as a form of comprehension. This notion is shown to be instrumental in giving a systematic and abstract proof of the existence of limits for coalgebras—proved earlier by Worrell and by Gumm & Schröder. These insights, in dual form, are used to reinvestigate colimits for algebras in terms of “least quotient algebras”—leading to a uniform approach to limits of coalgebras and colimits of algebras. Finally, at an abstract level of fibrations, an equivalence is established between having greatest subcoalgebras (in a base category of types) and greatest invariants (in a total category of predicates).     

Bisimulation from Open Maps

An abstract definition of bisimulation is presented. It makes possible a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets), and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner's strong bisimulation. On event structures it explains and leads to a strengthening of the history-preserving bisimulation of Rabinovitch and Traktenbrot and van Glabeek and Goltz. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has “refinement” operators. The general approach yields a logic, generalising Hennessy–Milner logic, which is characteristic for the generalised notion of bisimulation.     

Bisimulation and Hidden Algebra

A hidden algebra is a special case of coalgebra. A hidden congruence on a hidden algebra corresponds to a bisimulation equivalence on the corresponding coalgebra. The paper generalizes the notion of hidden congruence to that of hidden bisimulation between two different hidden algebras. We first define hidden bisimulation between two hidden algebras having the same signature. A hidden bisimulation is in fact a bisimulation between the corresponding coalgebras. We then define hidden simulation between two hidden algebras having different signatures related by a vertical signature morphism. We prefer to call this relation simulation because it is unidirectional, due to the signature morphism. For the last case, the relationship between simulation and refinement is discussed.     

Bisimulation is two-way simulation

We give here a simple proof of the fact that on transition systems bisimulation is the equivalence relation generated by simulation via functions. The proof entirely rests on simple rules of the calculus of relations.     

Bisimulation for Labelled Markov Processes

In this paper we introduce a new class of labelled transition systems—labelled Markov processes— and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete. We assume that the state space is a certain type of common metric space called an analytic space. We show that our definition of probabilistic bisimulation generalizes the Larsen–Skou definition given for discrete systems. The formalism and mathematics is substantially different from the usual treatment of probabilistic process algebra. The main technical contribution of the paper is a logical characterization of probabilistic bisimulation. This study revealed some unexpected results, even for discrete probabilistic systems.

• Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition.

• We do not need any finite branching assumption, yet there is no need of infinitary conjunction.

We also show how to construct the maximal autobisimulation on a system. In the finite state case, this is just a state minimization construction. The proofs that we give are of an entirely different character than the typical proofs of these results. They use quite subtle facts about analytic spaces and appear, at first sight, to be entirely nonconstructive. Yet one can give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation.     

Bisimulation for Higher-Order Process Calculi

Ahigher-order process calculusis a calculus for communicating systems which contains higher-order constructs like communication of terms. We analyse the notion ofbisimulationin these calculi. We argue that both the standard definition of bisimulation (i.e., the one for CCS and related calculi), as well ashigher-order bisimulation[E. Astesiano, A. Giovini, and G. Reggio,in“STACS '88,” Lecture Notes in Computer Science, Vol. 294, pp. 207–226, Springer-Verlag, Berlin/New York, 1988; G. Boudol,in“TAPSOFT '89,” Lecture Notes in Computer Science, Vol. 351, pp. 149–161, Springer-Verlag, Berlin/New York, 1989; B. Thomsen, Ph.D. thesis, Dept. of Computing, Imperial College, 1990] are in general unsatisfactory, because of their over-discrimination. We propose and study a new form of bisimulation for such calculi, calledcontext bisimulation, which yields a more satisfactory discriminanting power. A drawback of context bisimulation is the heavy use of universal quantification in its definition, which is hard to handle in practice. To resolve this difficulty we introducetriggered bisimulationandnormal bisimulation, and we prove that they both coincide with context bisimulation. In the proof, we exploit thefactorisation theorem: When comparing the behaviour of two processes, it allows us to “isolate” subcomponents which might give differences, so that the analysis can be concentrated on them     

Notes on Generative Probabilistic Bisimulation

In this notes we consider the model of Generative Probabilistic Transition Systems, and Baier and Hermanns' notion of weak bisimulation defined over them. We prove that, if we consider any process algebra giving rise to a Probabilistic Transition System satisfying the condition of regularity and offering prefixing, interleaving, and guarded recursion, then the coarsest congruence that is contained in weak bisimulation is strong bisimulation.     

Bisimulation equivalence of differential-algebraic systems

In this paper, the notion of bisimulation relation for linear input-state-output systems is extended to general linear differential-algebraic (DAE) systems. Geometric control theory is used to derive a linear-algebraic characterisation of bisimulation relations, and an algorithm for computing the maximal bisimulation relation between two linear DAE systems. The general definition is specialised to the case where the matrix pencil sE ? A is regular. Furthermore, by developing a one-sided version of bisimulation, characterisations of simulation and abstraction are obtained.     

Logical Construction of Final Coalgebras

We prove that every finitary polynomial endofunctor of a category has a final coalgebra, provided that is locally Cartesian closed, it has finite coproducts and is an extensive category, it has a natural number object.     

Bisimulation and cocongruence for probabilistic systems

We introduce a new notion of bisimulation, called event bisimulation on labelled Markov processes (LMPs) and compare it with the, now standard, notion of probabilistic bisimulation, originally due to Larsen and Skou. Event bisimulation uses a sub σ-algebra as the basic carrier of information rather than an equivalence relation. The resulting notion is thus based on measurable subsets rather than on points: hence the name. Event bisimulation applies smoothly for general measure spaces; bisimulation, on the other hand, is known only to work satisfactorily for analytic spaces. We prove the logical characterization theorem for event bisimulation without having to invoke any of the subtle aspects of analytic spaces that feature prominently in the corresponding proof for ordinary bisimulation. These complexities only arise when we show that on analytic spaces the two concepts coincide. We show that the concept of event bisimulation arises naturally from taking the co-congruence point of view for probabilistic systems. We show that the theory can be given a pleasing categorical treatment in line with general coalgebraic principles. As an easy application of these ideas we develop a notion of “almost sure” bisimulation; the theory comes almost “for free” once we modify Giry’s monad appropriately.     

Computable Functions on Final Coalgebras

This paper tackles computability issues on final coalgebras and tries to shed light on the following two questions: First, which functions on final coalgebras are computable? Second, which formal system allows us to define all computable functions on final coalgebras?In particular, we give a definition of computability on final coalgebras, deriving from the theory of effective domains. We then establish the admissibility of coinductive definitions and of a generalised μ-operator. This gives rise to a formal system, in which every term denotes a computable function.