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-checking; Equivalence-checking; One-counter machines

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Verification of qualitative \(\mathbb Z\) constraints, Model checking memoryful linear-time logics over one-counter automata, A note on emptiness for alternating finite automata with a one-letter alphabet, Reachability in Succinct and Parametric 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