An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages

DOI10.1016/S0304-3975(97)00219-3zbMath0915.68058MaRDI QIDQ1276242

Thomas Wilke, Pierre Wolper, Doron A. Peled

Publication date: 30 March 1999

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

specification languageslinear temporal logicconcurrency theory

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55)

Related Items (13)

Realizability of concurrent recursive programs ⋮ Partial Order Reduction for Deep Bug Finding in Synchronous Hardware ⋮ Forward analysis and model checking for trace bounded WSTS ⋮ A note on a question of Peled and Wilke regarding stutter-invariant LTL ⋮ Partial-Order Reduction ⋮ Prognosis of \(\omega\)-languages for the diagnosis of *-languages: a topological perspective ⋮ Permutation rewriting and algorithmic verification ⋮ On projective and separable properties ⋮ On-the-Fly Stuttering in the Construction of Deterministic ω-Automata ⋮ The stuttering principle revisited ⋮ Realizability of Concurrent Recursive Programs ⋮ ENFORCING CONCURRENT TEMPORAL BEHAVIORS ⋮ Specification Languages for Stutter-Invariant Regular Properties

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A stubborn attack on state explosion
• Event fairness and non-interleaving concurrency
• Combining partial-order reductions with on-the-fly model-checking.
• A syntactic congruence for rational \(\omega\)-languages
• The complementation problem for Büchi automata with applications to temporal logic
• Automata-theoretic techniques for modal logics of programs
• Verification of distributed programs using representative interleaving sequences
• Proving partial order properties
• Reasoning about infinite computations
• Rational and recognizable complex trace languages
• An expressively complete linear time temporal logic for Mazurkiewicz traces
• Temporal logic can be more expressive
• The complexity of propositional linear temporal logics
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• An algorithmic approach for checking closure properties of Ω-regular languages

This page was built for publication: An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages