Model Checking Freeze LTL over One-Counter Automata

DOI10.1007/978-3-540-78499-9_34zbMath1139.68038OpenAlexW1738870074MaRDI QIDQ5458381

Ranko Lazić, Arnaud Sangnier, Stéphane P. Demri

Publication date: 11 April 2008

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-540-78499-9_34

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items (5)

Countdown games, and simulation on (succinct) one-counter nets ⋮ The decision problem for some logics for finite words on infinite alphabets ⋮ Process-centric views of data-driven business artifacts ⋮ Model checking memoryful linear-time logics over one-counter automata ⋮ Finite \(n\)-tape automata over possibly infinite alphabets: Extending a theorem of Eilenberg et al.

This page was built for publication: Model Checking Freeze LTL over One-Counter Automata