The complexity of flat freeze LTL

DOI10.4230/LIPICS.CONCUR.2017.33zbMATH Open1442.68102OpenAlexW2963712282MaRDI QIDQ5111647FDOQ5111647

Benedikt Bollig, Arnaud Sangnier, Karin Quaas

Publication date: 27 May 2020

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

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

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)

Cites Work

• On Expressiveness and Complexity in Real-Time Model Checking
• LTL with the freeze quantifier and register automata
• Two-variable logic on data words
• Title not available (Why is that?)
• Title not available (Why is that?)
• Reachability in Two-Clock Timed Automata Is PSPACE-Complete
• Hierarchies of complete problems
• Parametric real-time reasoning
• Title not available (Why is that?)
• Term Rewriting and Applications
• The effects of bounding syntactic resources on Presburger LTL
• Model Checking Succinct and Parametric One-Counter Automata
• Branching-Time Model Checking of Parametric One-Counter Automata
• Reachability in Succinct and Parametric One-Counter Automata
• On parametric timed automata and one-counter machines
• Deterministic one-counter automata
• On the freeze quantifier in Constraint LTL: Decidability and complexity
• Two-Way Tree Automata Solving Pushdown Games
• When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
• Alternation Elimination by Complementation (Extended Abstract)
• Foundations of Software Science and Computation Structures
• Model checking memoryful linear-time logics over one-counter automata
• Path Checking for MTL and TPTL over Data Words
• Simulation problems over one-counter nets
• Branching-time model checking of one-counter processes and timed automata
• Title not available (Why is that?)
• Distributed Timed Automata with Independently Evolving Clocks

Cited In (3)

• Model Checking Freeze LTL over One-Counter Automata
• Title not available (Why is that?)
• Title not available (Why is that?)

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)