Three logics for branching bisimulation

From MaRDI portal
Publication:4369871

DOI10.1145/201019.201032zbMath0886.68064OpenAlexW2107144615MaRDI QIDQ4369871

Rocco De Nicola, Frits W. Vaandrager

Publication date: 2 February 1998

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/1370



Related Items

Characteristic formulae for fixed-point semantics: a general framework, An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation, Model independent approach to probabilistic models, Branching time and orthogonal bisimulation equivalence, Operational semantics for Petri net components, Partial-Order Reduction, Abstraction and Abstraction Refinement, Model Checking Value-Passing Modal Specifications, Deriving Inverse Operators for Modal Logic, Branching bisimilarity is an equivalence indeed!, Geometric Model Checking of Continuous Space, Compositional verification of concurrent systems by combining bisimulations, Computing Stuttering Simulations, Comparative branching-time semantics for Markov chains, Formal verification technique for grid service chain model and its application, Two implementation relations and the correctness of communicating replicated processes, Embedding of biological regulatory networks and property preservation, Unnamed Item, All congruences below stability-preserving fair testing or CFFD, A complete axiomatization of weighted branching bisimulation, When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus, Partial-order reduction in the weak modal mu-calculus, A state/event-based model-checking approach for the analysis of abstract system properties, An accessible verification environment for UML models of services, Modelling mutual exclusion in a process algebra with time-outs, An automated quantitative information flow analysis for concurrent programs, Theory of interaction, Compositional Specification in Rewriting Logic, A Spatial Logic for Simplicial Models, Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity, Equivalence checking 40 years after: a review of bisimulation tools, Apartness and distinguishing formulas in Hennessy-Milner logic, Cartesian difference categories, A formal model for service-oriented interactions, Automated temporal equilibrium analysis: verification and synthesis of multi-player games, Unnamed Item, Unnamed Item, Generalizing the Paige-Tarjan algorithm by abstract interpretation, Compositionality in state space verification methods, Monitoring and recovery for web service applications, Studying equivalences of transition systems with algebraic tools, Translations between modal logics of reactive systems, Universal axioms for bisimulations, Universal extensions to simulate specifications, An O(m log n) algorithm for branching bisimilarity on labelled transition systems, Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities, Automatic verification of distributed systems: the process algebra approach., Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes, Simulation refinement for concurrency verification, Dynamic consistency in process algebra: from paradigm to ACP, Probabilistic divide \& congruence: branching bisimilarity, Algebraic characterizations of trace and decorated trace equivalences over tree-like structures, Branching bisimulation for probabilistic systems: characteristics and decidability, Smaller Abstractions for ∀CTL* without Next, Encapsulating deontic and branching time specifications, On Compositionality, Efficiency, and Applicability of Abstraction in Probabilistic Systems, A general approach to comparing infinite-state systems with their finite-state specifications, Characterizing right inverses for spatial constraint systems with applications to modal logic, Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints, Folk Theorems on the Correspondence between State-Based and Event-Based Systems, Egalitarian State-Transition Systems, Game-theoretic simulation checking tool, Branching bisimulation congruence for probabilistic systems, Towards a unified view of bisimulation: A comparative study, A Logical Process Calculus, Raiders of the lost equivalence: probabilistic branching bisimilarity, Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal, An efficient simulation algorithm based on abstract interpretation, Unnamed Item, From EU Projects to a Family of Model Checkers, Simulation for lattice-valued doubly labeled transition systems, Next-preserving branching bisimulation, Translating Java for multiple model checkers: The Bandera back-end