The complexity of flat freeze LTL

DOI10.4230/LIPICS.CONCUR.2017.33MaRDI QIDQ5111647zbMATH OpenOpenAlexFDO

Authors Benedikt Bollig, Karin Quaas, Arnaud Sangnier

Publication date 27 May 2020

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2017/7799/

zbMATH Keywords

model checkingone-counter automatafreeze LTL

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• The complexity of flat freeze LTL
• Model checking flat freeze LTL on one-counter automata
• Model checking flat Freeze LTL on one-counter automata
• Model Checking Freeze LTL over One-Counter Automata
• When model-checking freeze LTL over counter machines becomes decidable

Cites work

• scientific article; zbMATH DE number 1670482 (Why is no real title available?)
• scientific article; zbMATH DE number 1670767 (Why is no real title available?)
• scientific article; zbMATH DE number 1223729 (Why is no real title available?)
• Alternation Elimination by Complementation (Extended Abstract)
• Branching-time model checking of one-counter processes and timed automata
• Branching-time model checking of parametric one-counter automata
• Deterministic one-counter automata
• Distributed timed automata with independently evolving clocks
• Foundations of Software Science and Computation Structures
• Hierarchies of complete problems
• LTL with the freeze quantifier and register automata
• Model checking flat freeze LTL on one-counter automata
• Model checking memoryful linear-time logics over one-counter automata
• Model checking succinct and parametric one-counter automata
• On Expressiveness and Complexity in Real-Time Model Checking
• On parametric timed automata and one-counter machines
• On the freeze quantifier in Constraint LTL: Decidability and complexity
• Parametric real-time reasoning
• Reachability in Succinct and Parametric One-Counter Automata
• Reachability in two-clock timed automata is PSPACE-complete
• Simulation problems over one-counter nets
• Term Rewriting and Applications
• The effects of bounding syntactic resources on Presburger LTL
• Two-Way Tree Automata Solving Pushdown Games
• Two-variable logic on data words
• When model-checking freeze LTL over counter machines becomes decidable

Cited in

(6)

• The complexity of flat freeze LTL
• Model Checking Freeze LTL over One-Counter Automata
• When model-checking freeze LTL over counter machines becomes decidable
• scientific article; zbMATH DE number 7559494 (Why is no real title available?)
• Model checking flat freeze LTL on one-counter automata
• Model checking flat Freeze LTL on one-counter automata

This page was built for publication: The complexity of flat freeze LTL

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