zbMATH — the first resource for mathematics

DP lower bounds for equivalence-checking and model-checking of one-counter automata. (English) Zbl 1078.68087
Summary: We present a general method for proving DP-hardness of problems related to formal verification of one-counter automata. For this we show a reduction of the SAT-UNSAT problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment contains only special formulas with one free variable, and is particularly apt for transforming to simulation-like equivalences on one-counter automata. In this way we show that the membership problem for any relation subsuming bisimilarity and subsumed by simulation preorder is DP-hard (even) for one-counter nets (where the counter cannot be tested for zero). We also show DP-hardness for deciding simulation between one-counter automata and finite-state systems (in both directions), and for the model-checking problem with one-counter nets and the branching-time temporal logic EF.

68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Abdulla, P.; Čerāns, K., Simulation is decidable for one-counter nets, (), 253-268 · Zbl 0940.68055
[2] Bach, E.; Shallit, J., Algorithmic number theory, Efficient algorithms, vol. 1, (1996), The MIT Press Cambridge, MA · Zbl 0873.11070
[3] Bergstra, J.; Klop, J., Algebra of communicating processes with abstraction, Theoretical computer science, 37, 77-121, (1985) · Zbl 0579.68016
[4] Bouajjani, A.; Habermehl, P.; Mayr, R., Automatic verification of recursive procedures with one integer parameter, (), 198-211 · Zbl 1005.68096
[5] S. Christensen, Decidability and decomposition in process algebras, Ph.D. Thesis, University of Edinburgh, 1993
[6] Emerson, E., Temporal and modal logic, Handbook of theoretical computer science, B, 995-1072, (1991) · Zbl 0900.03030
[7] Esparza, J.; Knoop, J., An automata-theoretic approach to interprocedural data-flow analysis, (), 14-30
[8] Jančar, P., Decidability of bisimilarity for one-counter processes, Information and computation, 158, 1, 1-17, (2000) · Zbl 1046.68621
[9] Jančar, P.; Kučera, A.; Mayr, R., Deciding bisimulation-like equivalences with finite-state processes, Theoretical computer science, 258, 1-2, 409-433, (2001) · Zbl 0974.68131
[10] Jančar, P.; Kučera, A.; Moller, F., Simulation and bisimulation over one-counter processes, (), 334-345 · Zbl 0962.68121
[11] Jančar, P.; Kučera, A.; Moller, F.; Sawa, Z., Equivalence-checking with one-counter automata: a generic method for proving lower bounds, (), 172-186 · Zbl 1077.68653
[12] Jančar, P.; Moller, F.; Sawa, Z., Simulation problems for one-counter machines, (), 404-413 · Zbl 0963.68094
[13] Kozen, D., Results on the propositional μ-calculus, Theoretical computer science, 27, 333-354, (1983) · Zbl 0553.03007
[14] Kučera, A., Efficient verification algorithms for one-counter processes, (), 317-328 · Zbl 0973.68163
[15] Kučera, A., On simulation-checking with sequential systems, (), 133-148 · Zbl 0987.68045
[16] Kučera, A.; Mayr, R., Simulation preorder over simple process algebras, Information and computation, 173, 2, 184-198, (2002) · Zbl 1009.68083
[17] Mayr, R., Strict lower bounds for model checking BPA, Entcs, 18, (1998)
[18] Mayr, R., Undecidability of weak bisimulation equivalence for 1-counter processes, (), 570-583 · Zbl 1039.68084
[19] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[20] Papadimitriou, C., Computational complexity, (1994), Addison-Wesley Reading, MA · Zbl 0833.68049
[21] Park, D., Concurrency and automata on infinite sequences, (), 167-183
[22] Stirling, C., Modal and temporal logics, Handbook of logic in computer science, 2, 477-563, (1992)
[23] van Glabbeek, R., The linear time—branching time spectrum, Handbook of process algebra, 3-99, (1999) · Zbl 1035.68073
[24] Walukiewicz, I., Pushdown processes: games and model-checking, Information and computation, 164, 2, 234-263, (2001) · Zbl 1003.68072
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.