Compositional verification of concurrent systems by combining bisimulations
From MaRDI portal
Publication:2147689
DOI10.1007/S10703-021-00360-WOpenAlexW4231183851MaRDI QIDQ2147689FDOQ2147689
Frédéric Lang, Franco Mazzanti, Radu Mateescu
Publication date: 20 June 2022
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-03159616v2/file/Lang-Mateescu-Mazzanti-21.pdf
model checkingtemporal logicstate space reductionconcurrency theorymodal mu-calculuslabelled transition system
Cites Work
- Derivatives of Regular Expressions
- Propositional dynamic logic of regular programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Compositional verification of asynchronous concurrent systems using CADP
- Propositional dynamic logic of looping and converse is elementarily decidable
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Results on the propositional \(\mu\)-calculus
- Branching time and abstraction in bisimulation semantics
- Title not available (Why is that?)
- An automata theoretic decision procedure for the propositional mu- calculus
- Three logics for branching bisimulation
- Title not available (Why is that?)
- Sequential and distributed on-the-fly computation of weak tau-confluence
- Title not available (Why is that?)
- Confluence for process verification
- A partial order approach to branching time logic model checking.
- Title not available (Why is that?)
- Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems
- Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
- Partial-order reduction in the weak modal mu-calculus
Cited In (7)
- Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions
- On the complexity of verifying concurrent transition systems
- Title not available (Why is that?)
- \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics
- A Proof System for Compositional Verification of Probabilistic Concurrent Processes
- On the computation of counterexamples in compositional nonblocking verification
- Deriving Bisimulation Congruences for Conditional Reactive Systems
Uses Software
This page was built for publication: Compositional verification of concurrent systems by combining bisimulations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147689)