Pure future local temporal logics are expressively complete for Mazurkiewicz traces
type: Item
instance of: scholarly article
title: Pure future local temporal logics are expressively complete for Mazurkiewicz traces
zbMATH Open document ID: 1113.03016
author: Volker Diekert
author: Paul Gastin
published in: Information and Computation
publication date: 2007-01-22T00:00:00Z
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)].
reviewed by: Valentin Goranko
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 5117641
zbMATH Keywords: temporal logics
zbMATH Keywords: Mazurkiewicz traces
zbMATH Keywords: concurrency
zbMATH Keywords: expressive completeness
zbMATH Keywords: aperiodic trace language
MaRDI profile type: Publication
full work available at URL: j.ic.2006.07.002
OpenAlex ID: W2009852886
cites work: Q4737220
cites work: On the expressive power of temporal logic
cites work: LTL is expressively complete for Mazurkiewicz traces
cites work: Q4738286
cites work: Local temporal logic is expressively complete for cograph dependence alphabets
cites work: LATIN 2004: Theoretical Informatics
cites work: From local to global temporal logics over Mazurkiewicz traces.
cites work: Logical definability on infinite traces
cites work: CONCUR 2003 - Concurrency Theory
cites work: Q4737221
cites work: Mathematical Foundations of Computer Science 2003
cites work: Parallel Program Schemata and Maximal Parallelism I. Fundamental Results
cites work: Q5641083
cites work: Q4375802
cites work: A ν-calculus with local views for systems of sequential agents
cites work: TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION
cites work: Q3698327
cites work: First-order logic and star-free sets
cites work: On finite monoids having only trivial subgroups
cites work: Q4407441
cites work: An expressively complete linear time temporal logic for Mazurkiewicz traces
cites work: Star-free regular sets of ω-sequences
cites work: Q4219025
cites work: Q4251040
DOI: 10.1016/J.IC.2006.07.002
description: scientific article; zbMATH DE number 5117641