Local model checking in a logic for true concurrency

DOI10.1007/978-3-662-54458-7_24MaRDI QIDQ2988383zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Model checking a logic for true concurrency
• A logic for true concurrency
• A logic for true concurrency
• Automata for true concurrency properties
• scientific article; zbMATH DE number 218548

Cites work

• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• A logic for true concurrency
• An automata theoretic decision procedure for the propositional mu- calculus
• Concurrent bisimulations in Petri nets
• Continuous Fragment of the mu-Calculus
• Event identifier logic
• scientific article; zbMATH DE number 4018370 (Why is no real title available?)
• scientific article; zbMATH DE number 1809623 (Why is no real title available?)
• scientific article; zbMATH DE number 4210118 (Why is no real title available?)
• scientific article; zbMATH DE number 4074506 (Why is no real title available?)
• scientific article; zbMATH DE number 176758 (Why is no real title available?)
• scientific article; zbMATH DE number 1231616 (Why is no real title available?)
• scientific article; zbMATH DE number 794261 (Why is no real title available?)
• Local model checking in the modal mu-calculus
• Logics and Bisimulation Games for Concurrency, Causality and Conflict
• Modal logics and mu-calculi: An introduction
• Model-Checking Games for Fixpoint Logics with Partial Order Models
• On model checking for the -calculus and its fragments
• Refinement of actions and equivalence notions for concurrent systems
• Undecidability of domino games and hhp-bisimilarity.
• Unfoldings: A partial-order approach to model checking.
• Weak MSO: automata and expressiveness modulo bisimilarity

Cited in

(6)

• A logic for true concurrency
• Model checking a logic for true concurrency
• Model checking for event graphs and an event temporal logic
• A logic for true concurrency
• Un)Decidability for History Preserving True Concurrent Logics.
• Efficient model checking for LTL with partial order snapshots

This page was built for publication: Local model checking in a logic for true concurrency

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988383)