Pure future local temporal logics are expressively complete for Mazurkiewicz traces

From MaRDI portal

DOI10.1016/J.IC.2006.07.002MaRDI QIDQ859824zbMATH OpenOpenAlexFDO

Authors Volker Diekert, Paul Gastin

Publication date 22 January 2007

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

Full work available at URL https://doi.org/10.1016/j.ic.2006.07.002


zbMATH Keywords

aperiodic trace languageconcurrencyexpressive completenessMazurkiewicz tracestemporal logics

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)




Review text

The paper establishes expressive completeness of the pure future local temporal logic on Mazurkiewicz traces with respect to first-order definable trace languages. These are known to be aperiodic, so the main result follows from the proof that every aperiodic trace language is definable in pure future local temporal logic based on \textit{exists-next} and \textit{until} only. The proof and the result generalize \textit{T. Wilke}'s corresponding result on finite words [``Classifying discrete temporal properties, Lect. Notes Comput. Sci. 1563, 32--46 (1999; Zbl 0926.03018)].


Recommendations


Cites work


Cited in
(22)








This page was built for publication: Pure future local temporal logics are expressively complete for Mazurkiewicz traces

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

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Pure_future_local_temporal_logics_are_expressively_complete_for_Mazurkiewicz_traces&oldid=64890402"
Powered by MediaWiki