Model Checking Freeze LTL over One-Counter Automata

DOI10.1007/978-3-540-78499-9_34zbMATH Open1139.68038OpenAlexW1738870074MaRDI QIDQ5458381FDOQ5458381

Authors: Stéphane Demri, Ranko Lazić, Arnaud Sangnier 

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

Recommendations

• Model checking memoryful linear-time logics over one-counter automata
• Model checking flat freeze LTL on one-counter automata
• Model checking flat Freeze LTL on one-counter automata
• When model-checking freeze LTL over counter machines becomes decidable
• The complexity of flat freeze LTL

Mathematics Subject Classification ID

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

Cited In (12)

• Model checking flat freeze LTL on one-counter automata
• Model checking memoryful linear-time logics over one-counter automata
• The decision problem for some logics for finite words on infinite alphabets
• Finite \(n\)-tape automata over possibly infinite alphabets: Extending a theorem of Eilenberg et al.
• When model-checking freeze LTL over counter machines becomes decidable
• Countdown games, and simulation on (succinct) one-counter nets
• Model checking flat Freeze LTL on one-counter automata
• Model Checking FO(R) over One-Counter Processes and beyond
• The complexity of flat freeze LTL
• The complexity of flat freeze LTL
• Process-centric views of data-driven business artifacts
• The effects of bounding syntactic resources on Presburger LTL

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458381)