Branching-time model checking of parametric one-counter automata

DOI10.1007/978-3-642-28729-9_27MaRDI QIDQ2892786zbMATH OpenOpenAlexFDO

Authors Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell

Publication date 22 June 2012

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-642-28729-9_27

Mathematics Subject Classification ID

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

Recommendations

• Model checking succinct and parametric one-counter automata
• Branching-time model checking of one-counter processes and timed automata
• Branching-time model checking of one-counter processes
• Reachability in Succinct and Parametric One-Counter Automata
• On the complexity of model-checking branching and alternating-time temporal logics in one-counter systems

Cited in

(12)

• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Branching-time model checking of one-counter processes and timed automata
• Temporal specifications with accumulative values
• Branching-time model checking of one-counter processes
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Model checking succinct and parametric one-counter automata
• Model Checking Metric Temporal Logic over Automata with One Counter
• The complexity of flat freeze LTL
• The complexity of flat freeze LTL
• On parametric timed automata and one-counter machines
• Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures
• Constraint automata on infinite data trees: from CTL\((\mathbb{Z})\text{CTL}^*(\mathbb{Z})\) to decision procedures

This page was built for publication: Branching-time model checking of parametric one-counter automata

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