On the bisimulation proof method
From MaRDI portal
Publication:4236205
DOI10.1017/S0960129598002527zbMath0916.68057OpenAlexW2128995870MaRDI QIDQ4236205
Publication date: 22 March 1999
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129598002527
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Tower Induction and Up-to Techniques for CCS with Fixed Points ⋮ A symbolic decision procedure for symbolic alternating finite automata ⋮ Diacritical companions ⋮ Algorithms for Kleene algebra with converse ⋮ New up-to techniques for weak bisimulation ⋮ SPEC: An Equivalence Checker for Security Protocols ⋮ Encoding Asynchronous Interactions Using Open Petri Nets ⋮ Linear forwarders ⋮ Structural congruence for bialgebraic semantics ⋮ Extracting Proofs from Tabled Proof Search ⋮ Some congruence properties for \(\pi\)-calculus bisimilarities ⋮ Complete Lattices and Up-To Techniques ⋮ When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus ⋮ Distinguishing and relating higher-order and first-order processes by expressiveness ⋮ Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts ⋮ Parameterizing higher-order processes on names and processes ⋮ A fully abstract model for the \(\pi\)-calculus. ⋮ Proving language inclusion and equivalence by coinduction ⋮ Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus ⋮ Unnamed Item ⋮ Enhanced coalgebraic bisimulation ⋮ Up-to techniques for behavioural metrics via fibrations ⋮ Unnamed Item ⋮ Companions, Codensity and Causality ⋮ Metric Reasoning About $$\lambda $$-Terms: The General Case ⋮ Unnamed Item ⋮ Using bisimulation proof techniques for the analysis of distributed abstract machines ⋮ A Testing Theory for a Higher-Order Cryptographic Language ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Locality and interleaving semantics in calculi for mobile processes ⋮ Up-To Techniques for Behavioural Metrics via Fibrations ⋮ A general account of coinduction up-to ⋮ Generalised Coinduction ⋮ Elements of Stream Calculus ⋮ A process calculus for mobile ad hoc networks ⋮ On the observational theory of the CPS-calculus ⋮ On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems ⋮ Higher-order psi-calculi ⋮ Bisimulation proof methods in a path-based specification language for polynomial coalgebras ⋮ A hierarchy of equivalences for asynchronous calculi ⋮ Processes as formal power series: a coinductive approach to denotational semantics ⋮ Unnamed Item ⋮ Bisimulation and coinduction enhancements: a historical perspective ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ (Bi)simulations up-to characterise process semantics ⋮ Unnamed Item ⋮ On parameterization of higher-order processes ⋮ Process calculus based upon evaluation to committed form ⋮ GSOS for probabilistic transition systems ⋮ Unnamed Item ⋮ Corecursion up-to via causal transformations ⋮ Bisimulation and Co-induction: Some Problems ⋮ Simulations Up-to and Canonical Preorders
