The purpose of this paper is to investigate how bisimulation equivalence may be refined to give preorders which provide divergence-respecting approximation orderings between processes whose associated theories are as close as possible to that of bisimulation equivalence. The work is based on ideas first introduced in \textit{M. Hennessy} and \textit{G. Plotkin} [A term model for CCS, Lecture Notes in Comput. Sci. 88, Springer-Verlag (1980; Zbl 0479.68011)] and \textit{R. Milner} [A modal characterization of observable machine-behaviour, Lecture Notes in Comput. Sci. 112 (1981; Zbl 0474.68074)]. The paper is divided into five sections, the first being an introduction. Section 2 contains characterizations of the largest precongruence relations included in the latter three preorders, and Sections 3 and 4 present axiomatizations of these relations of the classes of finite closed terms and sequential terms of CCS, respectively. The final section contains an example illustrating how the theory of one of the preorders may be used as the basis of a verification technique.
- A calculus of communicating systems
- scientific article; zbMATH DE number 4060694 (Why is no real title available?)
- scientific article; zbMATH DE number 3716792 (Why is no real title available?)
- scientific article; zbMATH DE number 3744561 (Why is no real title available?)
- scientific article; zbMATH DE number 3754002 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- Modal logics for communicating systems
- Observation equivalence as a testing equivalence
- Minimizing the number of transitions with respect to observation equivalence
- A note on the characterization of weak bisimulation congruence in CCS
- A compositional protocol verification using relativized bisimulation
- A complete axiomatisation for observational congruence of finite-state behaviours
- When is partial trace equivalence adequate?
- Essential transitions to bisimulation equivalences
- A general conservative extension theorem in process algebras with inequalities
- A semantic theory for value-passing processes based on the late approach
- Finite axiom systems for testing preorder and De Simone process languages
- Bisimulation indexes and their applications
- Logics for bisimulation and divergence
- Decoding choice encodings
- Ordered SOS process languages for branching and eager bisimulations
- Process languages with discrete relative time based on the ordered SOS format and rooted eager bisimulation
- Power simulation and its relation to traces and failures refinement
- Ensuring liveness properties of distributed systems: open problems
- Counting nondeterministic computations
- Divide and congruence. III: From decomposition of modal formulas to preservation of stability and divergence
- Next-preserving branching bisimulation
- Testing equivalence as a bisimulation equivalence
- Axiomatizing weak simulation semantics over BCCSP
- Deciding orthogonal bisimulation
- Axiomatising divergence
- Reactive bisimulation semantics for a process algebra with timeouts
- A characterization of finitary bisimulation
- Axiomatizing weak ready simulation semantics over BCCSP
- Generalized Bisimulation Metrics
- Distributed bisimulations
- Bisimulation Congruences in the Calculus of Looping Sequences
- Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation
- Bisimulation can't be traced
- scientific article; zbMATH DE number 1500662 (Why is no real title available?)
- scientific article; zbMATH DE number 1759617 (Why is no real title available?)
- scientific article; zbMATH DE number 7015161 (Why is no real title available?)
- scientific article; zbMATH DE number 2086654 (Why is no real title available?)
- INQUISITIVE BISIMULATION
- scientific article; zbMATH DE number 7559462 (Why is no real title available?)
- Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations.
- CPO models for a class of GSOS languages
- Divide and congruence. III: Stability \& divergence
- On convergence-sensitive bisimulation and the embedding of CCS in timed CCS
- Confluence thanks to extensional determinism
- Analyzing divergence in bisimulation semantics
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- A randomized encoding of the \(\pi\)-calculus with mixed choice
- Communicating Sequential Processes. The First 25 Years
- The largest respectful function
- Non-deterministic structures of computation
- An intensional characterization of the largest bisimulation
- A fully abstract denotational model for observational precongruence
- Bisimulation on speed: Worst-case efficiency
- A fully abstract denotational model for observational precongruence
- Modal and temporal logics for processes
- Stepwise development of process-algebraic specifications in decorated trace semantics
- Theory of interaction
- On the expressiveness of interaction
- The equational theory of prebisimilarity over basic CCS with divergence
This page was built for publication: Bisimulation and divergence
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q750163)
