scientific article; zbMATH DE number 7003191

DOI10.23638/LMCS-14(4:20)2018zbMath1405.68187arXiv1606.02643MaRDI QIDQ4611376

Antonia Lechner, Amaury Pouly, Joël Ouaknine, James Worrell, Richard Mayr

Publication date: 18 January 2019

Full work available at URL: https://arxiv.org/abs/1606.02643

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

reachabilityPresburger arithmeticone-counter automatadisequality testsFreeze LTL

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)

Cites Work

• Unnamed Item
• On the freeze quantifier in Constraint LTL: Decidability and complexity
• Model checking memoryful linear-time logics over one-counter automata
• Reachability in two-clock timed automata is PSPACE-complete
• LTL with the freeze quantifier and register automata
• Reachability in Succinct and Parametric One-Counter Automata
• On Expressiveness and Complexity in Real-Time Model Checking
• When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
• New Decidability Results Concerning Two-Way Counter Machines
• Automated Technology for Verification and Analysis

This page was built for publication: