Compositional verification of concurrent systems by combining bisimulations

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

zbMATH Keywords

model checkingtemporal logiclabelled transition systemstate space reductionconcurrency theorymodal mu-calculus

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• CADP
• Exp.Open
• LNT2LOTOS

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