Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
From MaRDI portal
Publication:5164168
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
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