A note on a question of Peled and Wilke regarding stutter-invariant LTL

DOI10.1016/S0020-0190(00)00113-7zbMath1339.68166MaRDI QIDQ294841

Kousha Etessami

Publication date: 16 June 2016

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

Full work available at URL: http://www.sciencedirect.com/science/article/pii/S0020019000001137?np=y

zbMATH Keywords

specification languagestemporal logicnext operatorefficient translationstutter-invariance

Mathematics Subject Classification ID

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

Related Items

On-the-Fly Stuttering in the Construction of Deterministic ω-Automata ⋮ The stuttering principle revisited ⋮ A note on stutter-invariant PLTL ⋮ Specification Languages for Stutter-Invariant Regular Properties

Cites Work

• Unnamed Item
• Stutter-invariant temporal properties are expressible without the next-time operator
• An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages
• The complexity of propositional linear temporal logics