Equivalence checking 40 years after: a review of bisimulation tools
From MaRDI portal
Publication:6163887
DOI10.1007/978-3-031-15629-8_13zbMath1524.68189MaRDI QIDQ6163887
Publication date: 26 July 2023
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Computing strong and weak bisimulations for psi-calculi
- Computing maximal weak and other bisimulations
- Bisimulation on speed: Worst-case efficiency
- Confluence for process verification
- A brief history of Timed CSP
- Symbolic bisimulations
- Bisimulation minimization and symbolic model checking
- Interactive Markov chains. And the quest for quantified quality
- On the computational complexity of bisimulation, redux
- Game-theoretic simulation checking tool
- Algèbre de processus et synchronisation
- Automated analysis of mutual exclusion algorithms using CCS
- CCS expressions, finite state processes, and three problems of equivalence
- An implementation of an efficient algorithm for bisimulation equivalence
- Automatic verification of distributed systems: the process algebra approach.
- Calculi for synchrony and asynchrony
- Algebra of communicating processes with abstraction
- A calculus of communicating systems
- Bisimulation through probabilistic testing
- A calculus of mobile processes. I
- A calculus of mobile processes. II
- Structured operational semantics and bisimulation as a congruence
- A formal definition of time in LOTOS
- A theory of timed automata
- Model checking and boolean graphs
- Automatizing parametric reasoning on distributed concurrent systems
- Testing equivalences for processes
- Compositional minimisation of finite state systems using interface specifications
- A partial order approach to branching time logic model checking.
- Verification of the link layer protocol of the IEEE-1394 serial bus (FireWire): An experiment with E-LOTOS
- Kronos: A verification tool for real-time systems
- Protocol verification with the Aldébaran toolset
- A verification tool developer's vade mecum.
- The origins of structural operational semantics
- A structural approach to operational semantics
- Branching time and orthogonal bisimulation equivalence
- An efficient algorithm for computing bisimulation equivalence
- Symbolic transition graph and its early bisimulation checking algorithms for the \(\pi\)-calculus
- Computing bisimulations for finite-control \(\pi\)-calculus
- Automated compositional Markov chain generation for a plain-old telephone system
- An \(O(m\log n)\) algorithm for stuttering equivalence and branching bisimulation
- Bisimulation and coinduction enhancements: a historical perspective
- A parallel relation-based algorithm for symbolic bisimulation minimization
- Compositional verification of asynchronous concurrent systems using CADP
- Bisimulation for labelled Markov processes
- An efficient algorithm to determine probabilistic bisimulation
- Compositional Bisimulation Minimization for Interval Markov Decision Processes
- Branching Bisimulation Games
- AN EFFICIENT FULLY SYMBOLIC BISIMULATION ALGORITHM FOR NON-DETERMINISTIC SYSTEMS
- Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems
- SMT-Based Bisimulation Minimisation of Markov Models
- Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time
- CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
- The How and Why of Interactive Markov Chains
- SPEC: An Equivalence Checker for Security Protocols
- Sigref – A Symbolic Bisimulation Tool Box
- Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems
- On the Minimisation of Acyclic Models
- Concurrency and Composition in a Stochastic World
- Refined Interfaces for Compositional Verification
- Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment
- Towards Performance Prediction of Compositional Models in Industrial GALS Designs
- CIRCAL and the representation of communication, concurrency, and time
- Graph-Based Algorithms for Boolean Function Manipulation
- Process algebra for synchronous communication
- A Theory of Communicating Sequential Processes
- Three Partition Refinement Algorithms
- Formal verification of parallel programs
- Three logics for branching bisimulation
- Branching time and abstraction in bisimulation semantics
- An algebra-based method to associate rewards with EMPA terms
- Hybrid automata with finite bisimulations
- Compositional performance modelling with the TIPPtool
- Construction and Analysis of Transition Systems with MEC
- Rank-Based Symbolic Bisimulation
- Verification and comparison of transition systems
- Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs
- From LOTOS to LNT
- Model-checking for real-time systems
- An O(m log n) algorithm for branching bisimilarity on labelled transition systems
- Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
- Checking equivalences between concurrent systems of finite agents (Extended abstract)
- From μCRL to mCRL2
- An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Validation of Stochastic Systems
- Validation of Stochastic Systems
- An Overview of the mCRL2 Toolset and Its Recent Advances
- A Compositional Approach to Performance Modelling
- Tools and Algorithms for the Construction and Analysis of Systems
- Symmetry Reduction for Probabilistic Model Checking
- On-the-Fly Branching Bisimulation Minimization for Compositional Analysis
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- A Symbolic Algorithm for Optimal Markov Chain Lumping
- Generic tools for verifying concurrent systems
- Symbolic transition graph with assignment
- Bisimulation by Partitioning Is Ω((m+n)log n).
- Probabilistic bisimulation for parameterized systems (with applications to verifying anonymous protocols)
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
