Equivalence checking 40 years after: a review of bisimulation tools
From MaRDI portal
(Redirected from Publication:6163887)
Recommendations
- Simulation relations and applications in formal methods
- Tools and Algorithms for the Construction and Analysis of Systems
- Equivalence-checking with infinite-state systems: techniques and results
- Testing equivalence as a bisimulation equivalence
- Equivalence and preorder checking for finite-state systems
Cites work
- A brief history of Timed CSP
- A calculus of communicating systems
- A calculus of mobile processes. I
- A calculus of mobile processes. II
- A Compositional Approach to Performance Modelling
- A distributed algorithm for strong bisimulation reduction of state spaces
- A formal definition of time in LOTOS
- A parallel relation-based algorithm for symbolic bisimulation minimization
- A partial order approach to branching time logic model checking.
- A state space distribution policy based on abstract interpretation
- A structural approach to operational semantics
- A Symbolic Algorithm for Optimal Markov Chain Lumping
- A symbolic approach to value-passing processes
- A Theory of Communicating Sequential Processes
- A theory of timed automata
- A verification tool developer's vade mecum.
- Algebra of communicating processes with abstraction
- Algèbre de processus et synchronisation
- An O(m n) algorithm for computing stuttering equivalence and branching bisimulation
- An O(m n) algorithm for branching bisimilarity on labelled transition systems
- An \(O(m\log n)\) algorithm for stuttering equivalence and branching bisimulation
- An algebra-based method to associate rewards with EMPA terms
- An efficient algorithm for computing bisimulation equivalence
- An efficient algorithm to determine probabilistic bisimulation
- An efficient fully symbolic bisimulation algorithm for non-deterministic systems
- An implementation of an efficient algorithm for bisimulation equivalence
- An overview of the mCRL2 toolset and its recent advances
- Automated analysis of mutual exclusion algorithms using CCS
- Automated compositional Markov chain generation for a plain-old telephone system
- Automatic verification of distributed systems: the process algebra approach.
- Automatizing parametric reasoning on distributed concurrent systems
- Bisimulation and coinduction enhancements: a historical perspective
- Bisimulation by Partitioning Is Ω((m+n)log n).
- Bisimulation for labelled Markov processes
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Bisimulation minimization and symbolic model checking
- Bisimulation on speed: Worst-case efficiency
- Bisimulation through probabilistic testing
- Branching bisimulation games
- Branching time and abstraction in bisimulation semantics
- Branching time and orthogonal bisimulation equivalence
- CADP 2010: a toolbox for the construction and analysis of distributed processes
- Calculi for synchrony and asynchrony
- CCS expressions, finite state processes, and three problems of equivalence
- Checking equivalences between concurrent systems of finite agents (extended abstract)
- CIRCAL and the representation of communication, concurrency, and time
- Compositional bisimulation minimization for interval Markov decision processes
- Compositional minimisation of finite state systems using interface specifications
- Compositional performance modelling with the TIPPtool
- Compositional verification of asynchronous concurrent systems using CADP
- Computer Aided Verification
- Computing bisimulations for finite-control -calculus
- Computing maximal weak and other bisimulations
- Computing strong and weak bisimulations for psi-calculi
- Concurrency and composition in a stochastic world
- Confluence for process verification
- Construction and Analysis of Transition Systems with MEC
- Deciding probabilistic automata weak bisimulation in polynomial time
- Distributed branching bisimulation reduction of state spaces
- Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems
- Formal verification of parallel programs
- From CRL to mCRL2: motivation and outline
- From LOTOS to LNT
- Game-theoretic simulation checking tool
- Generating BDDs for symbolic model checking in CCS
- Generic tools for verifying concurrent systems
- Graph-Based Algorithms for Boolean Function Manipulation
- scientific article; zbMATH DE number 1629934 (Why is no real title available?)
- scientific article; zbMATH DE number 4050942 (Why is no real title available?)
- scientific article; zbMATH DE number 3716792 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 58291 (Why is no real title available?)
- scientific article; zbMATH DE number 140247 (Why is no real title available?)
- scientific article; zbMATH DE number 176726 (Why is no real title available?)
- scientific article; zbMATH DE number 177252 (Why is no real title available?)
- scientific article; zbMATH DE number 177262 (Why is no real title available?)
- scientific article; zbMATH DE number 177514 (Why is no real title available?)
- scientific article; zbMATH DE number 177515 (Why is no real title available?)
- scientific article; zbMATH DE number 177532 (Why is no real title available?)
- scientific article; zbMATH DE number 177824 (Why is no real title available?)
- scientific article; zbMATH DE number 177845 (Why is no real title available?)
- scientific article; zbMATH DE number 3514781 (Why is no real title available?)
- scientific article; zbMATH DE number 1283472 (Why is no real title available?)
- scientific article; zbMATH DE number 1306878 (Why is no real title available?)
- scientific article; zbMATH DE number 526071 (Why is no real title available?)
- scientific article; zbMATH DE number 709540 (Why is no real title available?)
- scientific article; zbMATH DE number 1059329 (Why is no real title available?)
- scientific article; zbMATH DE number 1956597 (Why is no real title available?)
- scientific article; zbMATH DE number 2080068 (Why is no real title available?)
- scientific article; zbMATH DE number 1497783 (Why is no real title available?)
- scientific article; zbMATH DE number 1786475 (Why is no real title available?)
- scientific article; zbMATH DE number 1796125 (Why is no real title available?)
- scientific article; zbMATH DE number 1796138 (Why is no real title available?)
- scientific article; zbMATH DE number 7015117 (Why is no real title available?)
- scientific article; zbMATH DE number 2087800 (Why is no real title available?)
- scientific article; zbMATH DE number 1905121 (Why is no real title available?)
- scientific article; zbMATH DE number 2090149 (Why is no real title available?)
- scientific article; zbMATH DE number 2102728 (Why is no real title available?)
- scientific article; zbMATH DE number 2102729 (Why is no real title available?)
- scientific article; zbMATH DE number 1390247 (Why is no real title available?)
- scientific article; zbMATH DE number 1435981 (Why is no real title available?)
- scientific article; zbMATH DE number 7559464 (Why is no real title available?)
- scientific article; zbMATH DE number 3212004 (Why is no real title available?)
- scientific article; zbMATH DE number 956807 (Why is no real title available?)
- Hybrid automata with finite bisimulations
- Interactive Markov chains. And the quest for quantified quality
- Kronos: A verification tool for real-time systems
- Model checking and boolean graphs
- Model-checking for real-time systems
- On the computational complexity of bisimulation, redux
- On the Minimisation of Acyclic Models
- On-the-Fly Branching Bisimulation Minimization for Compositional Analysis
- Partial model checking using networks of labelled transition systems and Boolean equation systems
- Polynomial-time alternating probabilistic bisimulation for interval MDPs
- Probabilistic bisimulation for parameterized systems (with applications to verifying anonymous protocols)
- Process algebra for synchronous communication
- Protocol verification with the Aldébaran toolset
- Rank-based symbolic bisimulation: (and model checking)
- Refined Interfaces for Compositional Verification
- Sharp congruences adequate with temporal logics combining weak and strong modalities
- Sigref – A Symbolic Bisimulation Tool Box
- SMT-based bisimulation minimisation of Markov models
- SPEC: an equivalence checker for security protocols
- Specification and verification of a dynamic reconfiguration protocol for agent-based applications
- Structured operational semantics and bisimulation as a congruence
- Symbolic bisimulations
- Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment
- Symbolic transition graph and its early bisimulation checking algorithms for the \(\pi\)-calculus
- Symbolic transition graph with assignment
- Symmetry Reduction for Probabilistic Model Checking
- Testing equivalences for processes
- The Concurrency Workbench with priorities
- The how and why of interactive Markov chains
- The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
- The origins of structural operational semantics
- Three logics for branching bisimulation
- Three Partition Refinement Algorithms
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Towards Performance Prediction of Compositional Models in Industrial GALS Designs
- Validation of Stochastic Systems
- Validation of Stochastic Systems
- Verification and comparison of transition systems
- Verification of the link layer protocol of the IEEE-1394 serial bus (FireWire): An experiment with E-LOTOS
- “On the fly” verification of behavioural equivalences and preorders
Cited in
(2)
This page was built for publication: Equivalence checking 40 years after: a review of bisimulation tools
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6163887)
