Stutter-invariant temporal properties are expressible without the next-time operator

DOI10.1016/S0020-0190(97)00133-6zbMath1337.68170OpenAlexW2041743477MaRDI QIDQ290250

Thomas Wilke, Doron A. Peled

Publication date: 1 June 2016

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0020-0190(97)00133-6

zbMATH Keywords

specification languagestemporal logicnext operatorstutter invariance

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

A case study on parametric verification of failure detectors ⋮ A note on a question of Peled and Wilke regarding stutter-invariant LTL ⋮ Partial-Order Reduction ⋮ A note on the characterization of TL [EF] ⋮ Interleaving isotactics -- an equivalence notion on behaviour abstractions ⋮ Delay-dependent partial order reduction technique for real time systems ⋮ Invariance under stuttering in a temporal logic of actions ⋮ An application of temporal projection to interleaving concurrency ⋮ On projective and separable properties ⋮ On-the-Fly Stuttering in the Construction of Deterministic ω-Automata ⋮ On the complexity of linear temporal logic with team semantics ⋮ Partial order reduction for checking soundness of time workflow nets ⋮ Formal verification of an executable LTL model checker with partial order reduction ⋮ The stuttering principle revisited ⋮ Partial order reduction for state/event LTL with application to component-interaction automata ⋮ Covering Steps Graphs of Time Petri Nets ⋮ Deciding global partial-order properties ⋮ A note on stutter-invariant PLTL ⋮ Partial Order Reduction for State/Event LTL ⋮ Optimising the ProB model checker for B using partial order reduction ⋮ Craig Interpolation for Linear Temporal Languages ⋮ A Reduction Theorem for the Verification of Round-Based Distributed Algorithms ⋮ Specification Languages for Stutter-Invariant Regular Properties ⋮ Safe Runtime Verification of Real-Time Properties ⋮ Slicing techniques for verification re-use ⋮ Verification of probabilistic systems with faulty communication ⋮ Taming past LTL and flat counter systems ⋮ Qualitative analysis of gene regulatory networks by temporal logic

Cites Work

• Unnamed Item
• A stubborn attack on state explosion
• Combining partial-order reductions with on-the-fly model-checking.
• Specifying Concurrent Program Modules
• An algorithmic approach for checking closure properties of Ω-regular languages