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 (73)
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
This page was built for publication: Three logics for branching bisimulation
