×

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.

MSC:

68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdulla, P.; Čerāns, K., Simulation is decidable for one-counter nets, (Proceedings of CONCUR’98. Proceedings of CONCUR’98, Lecture Notes in Computer Science, vol. 1466 (1998), Springer: Springer Berlin), 253-268 · Zbl 0940.68055
[2] Bach, E.; Shallit, J., Algorithmic number theory, Efficient Algorithms, vol. 1 (1996), The MIT Press: 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, (Proceedings of MFCS 2001. Proceedings of MFCS 2001, Lecture Notes in Computer Science, vol. 2136 (2001), Springer: Springer Berlin), 198-211 · Zbl 1005.68096
[5] S. Christensen, Decidability and decomposition in process algebras, Ph.D. Thesis, University of Edinburgh, 1993; 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, (Proceedings of FoSSaCS’99. Proceedings of FoSSaCS’99, Lecture Notes in Computer Science, vol. 1578 (1999), Springer: Springer Berlin), 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, (Proceedings of STACS 2000. Proceedings of STACS 2000, Lecture Notes in Computer Science, vol. 1770 (2000), Springer: Springer Berlin), 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, (Proceedings of FoSSaCS 2002. Proceedings of FoSSaCS 2002, Lecture Notes in Computer Science, vol. 2303 (2002), Springer: Springer Berlin), 172-186 · Zbl 1077.68653
[12] Jančar, P.; Moller, F.; Sawa, Z., Simulation problems for one-counter machines, (Proceedings of SOFSEM’99. Proceedings of SOFSEM’99, Lecture Notes in Computer Science, vol. 1725 (1999), Springer: Springer Berlin), 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, (Proceedings of ICALP 2000. Proceedings of ICALP 2000, Lecture Notes in Computer Science, vol. 1853 (2000), Springer: Springer Berlin), 317-328 · Zbl 0973.68163
[15] Kučera, A., On simulation-checking with sequential systems, (Proceedings of ASIAN 2000. Proceedings of ASIAN 2000, Lecture Notes in Computer Science, vol. 1961 (2000), Springer: Springer Berlin), 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, (Proceedings of ICALP 2003. Proceedings of ICALP 2003, Lecture Notes in Computer Science, vol. 2719 (2003), Springer: Springer Berlin), 570-583 · Zbl 1039.68084
[19] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[20] Papadimitriou, C., Computational Complexity (1994), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0833.68049
[21] Park, D., Concurrency and automata on infinite sequences, (Proceedings of the 5th GI Conference. Proceedings of the 5th GI Conference, Lecture Notes in Computer Science, vol. 104 (1981), Springer: Springer Berlin), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.