DP lower bounds for equivalence-checking and model-checking of one-counter automata

DOI10.1016/S0890-5401(03)00171-8zbMath1078.68087WikidataQ59556958 ScholiaQ59556958MaRDI QIDQ1887159

Zdeněk Sawa, Antonín Kučera, Petr Jančar, Faron Moller

Publication date: 23 November 2004

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

Model-checkingEquivalence-checkingOne-counter machines

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Countdown games, and simulation on (succinct) one-counter nets ⋮ A note on emptiness for alternating finite automata with a one-letter alphabet ⋮ Reachability in Succinct and Parametric One-Counter Automata ⋮ Verification of qualitative \(\mathbb Z\) constraints ⋮ Model checking memoryful linear-time logics over one-counter automata ⋮ Model Checking FO(R) over One-Counter Processes and beyond

Cites Work

• Results on the propositional \(\mu\)-calculus
• Algebra of communicating processes with abstraction
• Decidability of bisimilarity for one-counter processes.
• Pushdown processes: Games and model-checking
• Simulation preorder over simple process algebras
• Deciding bisimulation-like equivalences with finite-state processes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: DP lower bounds for equivalence-checking and model-checking of one-counter automata