LTL is expressively complete for Mazurkiewicz traces

DOI10.1006/jcss.2001.1817zbMath1013.68130OpenAlexW1992383908MaRDI QIDQ1608324

Volker Diekert, Paul Gastin

Publication date: 4 August 2002

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jcss.2001.1817

zbMATH Keywords

concurrencylinear temporal logic

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 (9)

Pure future local temporal logics are expressively complete for Mazurkiewicz traces ⋮ Finite-trace linear temporal logic: coinductive completeness ⋮ A survey on the local divisor technique ⋮ Specifying reversibility with \(\mathrm{TLA}^+\) ⋮ Local temporal logic is expressively complete for cograph dependence alphabets ⋮ From local to global temporal logics over Mazurkiewicz traces. ⋮ Unnamed Item ⋮ Testing Distributed Systems Through Symbolic Model Checking ⋮ Realizability of Concurrent Recursive Programs

Cites Work

• Logical definability on infinite traces
• An expressively complete linear time temporal logic for Mazurkiewicz traces
• Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets
• A ν-calculus with local views for systems of sequential agents
• TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: LTL is expressively complete for Mazurkiewicz traces