Satisfiability and model checking for MSO-definable temporal logics are in PSPACE.

DOI10.1007/B11938MaRDI QIDQ5900568zbMATH OpenOpenAlexFDO

Authors Paul Gastin, Dietrich Kuske

Publication date 30 March 2010

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

Full work available at URL https://doi.org/10.1007/b11938

Mathematics Subject Classification ID

Temporal logic (03B44) Analysis of algorithms and problem complexity (68Q25) 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

• Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces
• Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces
• CONCUR 2005 – Concurrency Theory
• scientific article; zbMATH DE number 2086684
• Temporal logics over linear time domains are in PSPACE

Cited in

(11)

• From local to global temporal logics over Mazurkiewicz traces.
• LTL over integer periodicity constraints
• The fixed-parameter tractability of model checking concurrent systems
• Temporal logics for concurrent recursive programs: satisfiability and model checking
• Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces
• Propositional Dynamic Logic for Message-Passing Systems
• Closing star-free closure
• Pure future local temporal logics are expressively complete for Mazurkiewicz traces
• An automata-theoretic approach to constraint LTL
• Verification of qualitative \(\mathbb Z\) constraints
• Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces

This page was built for publication: Satisfiability and model checking for MSO-definable temporal logics are in PSPACE.

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