Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities

DOI10.1007/978-3-030-45237-7_4zbMath1483.68233OpenAlexW3016368599MaRDI QIDQ5164168

Frédéric Lang, Franco Mazzanti, Radu Mateescu

Publication date: 10 November 2021

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-45237-7_4

zbMATH Keywords

model checkingbisimulationconcurrencymu-calculus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (2)

Compositional verification of concurrent systems by combining bisimulations ⋮ Equivalence checking 40 years after: a review of bisimulation tools

Cites Work

• Confluence for process verification
• Results on the propositional \(\mu\)-calculus
• Propositional dynamic logic of regular programs
• Weak confluence and \(\tau\)-inertness
• Selective mu-calculus and formula-based equivalence of transition systems
• Compositional verification of asynchronous concurrent systems using CADP
• Next-preserving branching bisimulation
• Nested-unit Petri nets
• Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems
• CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
• Branching Bisimilarity with Explicit Divergence
• Computation Tree Logic with Deadlock Detection
• Propositional dynamic logic of looping and converse is elementarily decidable
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• A Theory of Communicating Sequential Processes
• Three logics for branching bisimulation
• Branching time and abstraction in bisimulation semantics
• An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities