Local Model Checking in a Logic for True Concurrency

DOI10.1007/978-3-662-54458-7_24zbMath1486.68102OpenAlexW2613210537MaRDI QIDQ2988383

Paolo Baldan, Tommaso Padoan

Publication date: 19 May 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54458-7_24

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An automata theoretic decision procedure for the propositional mu- calculus
• Local model checking in the modal mu-calculus
• Undecidability of domino games and hhp-bisimilarity.
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Unfoldings: A partial-order approach to model checking.
• Concurrent bisimulations in Petri nets
• Model-Checking Games for Fixpoint Logics with Partial Order Models
• Continuous Fragment of the mu-Calculus
• Logics and Bisimulation Games for Concurrency, Causality and Conflict
• Weak MSO
• A Logic for True Concurrency
• Event Identifier Logic
• Refinement of actions and equivalence notions for concurrent systems
• On model checking for the \(\mu\)-calculus and its fragments