An expressively complete linear time temporal logic for Mazurkiewicz traces

DOI10.1006/INCO.2001.2956MaRDI QIDQ2506491zbMATH OpenOpenAlexFDO

Authors P. S. Thiagarajan, Igor Walukiewicz

Publication date 10 October 2006

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1006/inco.2001.2956

Mathematics Subject Classification ID

Temporal logic (03B44) 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

• scientific article; zbMATH DE number 1670825
• LTL is expressively complete for Mazurkiewicz traces
• Publication:4945225
• scientific article; zbMATH DE number 2086684
• scientific article; zbMATH DE number 1059327

Cites work

• A -calculus with local views for systems of sequential agents
• A logical study of distributed transition systems
• A stubborn attack on state explosion
• An algorithmic approach for checking closure properties of Ω-regular languages
• Asynchronous cellular automata for infinite traces
• scientific article; zbMATH DE number 747023 (Why is no real title available?)
• scientific article; zbMATH DE number 1223711 (Why is no real title available?)
• scientific article; zbMATH DE number 1114033 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 783754 (Why is no real title available?)
• scientific article; zbMATH DE number 803291 (Why is no real title available?)
• Logical definability on infinite traces
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Proving partial order properties
• The first order properties of products of algebraic systems

Cited in

(29)

• An algorithmic approach for checking closure properties of temporal logic specifications and -regular languages
• LTL is expressively complete for Mazurkiewicz traces
• Finite-trace linear temporal logic: coinductive completeness
• Model checking properties on reduced trace systems
• Local temporal logic is expressively complete for cograph dependence alphabets
• Difficult configurations -- on the complexity of LTrL
• Regular sets of infinite message sequence charts
• Comparing trace expressions and linear temporal logic for runtime verification
• Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic
• From local to global temporal logics over Mazurkiewicz traces.
• A theory of regular MSC languages
• scientific article; zbMATH DE number 1670825 (Why is no real title available?)
• Undecidability of partial order logics
• AN EXPRESSIVE EXTENSION OF TLC
• Testing Distributed Systems Through Symbolic Model Checking
• scientific article; zbMATH DE number 1059327 (Why is no real title available?)
• scientific article; zbMATH DE number 1114033 (Why is no real title available?)
• scientific article; zbMATH DE number 1136089 (Why is no real title available?)
• scientific article; zbMATH DE number 1969331 (Why is no real title available?)
• scientific article; zbMATH DE number 1500557 (Why is no real title available?)
• scientific article; zbMATH DE number 2086683 (Why is no real title available?)
• scientific article; zbMATH DE number 2086684 (Why is no real title available?)
• scientific article; zbMATH DE number 2087486 (Why is no real title available?)
• The Linear Temporal Logic of Rewriting Maude Model Checker
• scientific article; zbMATH DE number 1424035 (Why is no real title available?)
• It is easy to be wise after the event: communicating finite-state machines capture first-order logic with ``happened before
• Step traces
• Realizable temporal logics for web service choreography
• Pure future local temporal logics are expressively complete for Mazurkiewicz traces

This page was built for publication: An expressively complete linear time temporal logic for Mazurkiewicz traces

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