Compositional verification of concurrent systems by combining bisimulations
From MaRDI portal
Publication:2147689
DOI10.1007/s10703-021-00360-wOpenAlexW4231183851MaRDI QIDQ2147689
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 logiclabelled transition systemstate space reductionconcurrency theorymodal mu-calculus
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Sequential and distributed on-the-fly computation of weak tau-confluence
- Confluence for process verification
- Results on the propositional \(\mu\)-calculus
- An automata theoretic decision procedure for the propositional mu- calculus
- Propositional dynamic logic of regular programs
- A partial order approach to branching time logic model checking.
- Compositional verification of asynchronous concurrent systems using CADP
- Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems
- Propositional dynamic logic of looping and converse is elementarily decidable
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Three logics for branching bisimulation
- Branching time and abstraction in bisimulation semantics
- Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
- Derivatives of Regular Expressions
- Partial-order reduction in the weak modal mu-calculus
