When Model-Checking Freeze LTL over Counter Machines Becomes Decidable

DOI10.1007/978-3-642-12032-9_13zbMath1284.68394OpenAlexW203022780MaRDI QIDQ3557850

Stéphane P. Demri, Arnaud Sangnier

Publication date: 27 April 2010

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-12032-9_13

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Related Items (6)

Bisimulation equivalence and regularity for real-time one-counter automata ⋮ Unnamed Item ⋮ Temporal Specifications with Accumulative Values ⋮ Model checking memoryful linear-time logics over one-counter automata ⋮ Unnamed Item ⋮ The Complexity of Flat Freeze LTL

This page was built for publication: When Model-Checking Freeze LTL over Counter Machines Becomes Decidable