×

Counter machines and verification problems. (English) Zbl 1061.68095

Summary: We study various generalizations of reversal-bounded multicounter machines and show that they have decidable emptiness, infiniteness, disjointness, containment, and equivalence problems. The extensions include allowing the machines to perform linear-relation tests among the counters and parameterized constants (e.g., “Is \(3x-5y-2D_{1}+9D_{2}<12?\)”, where \(x,y\) are counters, and \(D_{1},D_{2}\) are parameterized constants). We believe that these machines are the most powerful machines known to date for which these decision problems are decidable. Decidability results for such machines are useful in the analysis of reachability problems and the verification/debugging of safety properties in infinite-state transition systems. For example, we show that (binary, forward, and backward) reachability and safety are solvable for these machines.

MSC:

68Q45 Formal languages and automata
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

ALGOL 60
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdulla, P.; Jonsson, B., Verifying programs with unreliable channels, Inform. Comput., 127, 2, 91-101 (1996) · Zbl 0856.68096
[2] Alur, R.; Dill, D., A theory of timed automata, Theoret. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071
[3] Baker, B.; Book, R., Reversal-bounded multipushdown machines, J. Comput. System Sci., 8, 315-332 (1974) · Zbl 0309.68043
[4] A. Bouajjani, J. Esparza, O. Maler, Reachability analysis of pushdown automata: application to model-checking, Proc. Internat. Conf. on Concurrency (CONCUR 1997), Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997, pp. 135-150.; A. Bouajjani, J. Esparza, O. Maler, Reachability analysis of pushdown automata: application to model-checking, Proc. Internat. Conf. on Concurrency (CONCUR 1997), Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997, pp. 135-150.
[5] G. Cece, A. Finkel, Programs with quasi-stable channels are effectively recognizable, Proc. 9th Internat. Conf. on Computer Aided Verification (CAV 1997), Lecture Notes in Computer Science, Vol. 1254, Springer, Berlin, 1997, pp. 304-315.; G. Cece, A. Finkel, Programs with quasi-stable channels are effectively recognizable, Proc. 9th Internat. Conf. on Computer Aided Verification (CAV 1997), Lecture Notes in Computer Science, Vol. 1254, Springer, Berlin, 1997, pp. 304-315.
[6] H. Comon, Y. Jurski, Multiple counters automata, safety analysis and Presburger arithmetic, Proc. 10th Internat. Conf. on Computer Aided Verification (CAV 1998), Lecture Notes in Computer Science, Vol. 1855, Springer, Berlin, 1998, pp. 268-279.; H. Comon, Y. Jurski, Multiple counters automata, safety analysis and Presburger arithmetic, Proc. 10th Internat. Conf. on Computer Aided Verification (CAV 1998), Lecture Notes in Computer Science, Vol. 1855, Springer, Berlin, 1998, pp. 268-279.
[7] Z. Dang, Binary reachability analysis of timed pushdown automata with dense clocks, Proc. 13th Internat. Conf. on Computer Aided Verification (CAV 2001), Lecture Notes in Computer Science, Vol. 2102, Springer, Berlin, 2001, pp. 506-518.; Z. Dang, Binary reachability analysis of timed pushdown automata with dense clocks, Proc. 13th Internat. Conf. on Computer Aided Verification (CAV 2001), Lecture Notes in Computer Science, Vol. 2102, Springer, Berlin, 2001, pp. 506-518. · Zbl 0991.68035
[8] Z. Dang, O.H. Ibarra, T. Bultan, R.A. Kemmerer, J. Su, Binary reachability analysis of discrete pushdown timed automata, Proc. 12th Internat. Conf. on Computer Aided Verification (CAV 2000), Lecture Notes in Computer Science, Vol. 1427, Springer, Berlin, 2000, pp. 69-84.; Z. Dang, O.H. Ibarra, T. Bultan, R.A. Kemmerer, J. Su, Binary reachability analysis of discrete pushdown timed automata, Proc. 12th Internat. Conf. on Computer Aided Verification (CAV 2000), Lecture Notes in Computer Science, Vol. 1427, Springer, Berlin, 2000, pp. 69-84. · Zbl 0974.68085
[9] Esparza, J., Decidability of model checking for infinite-state concurrent systems, Acta Inform., 34, 2, 85-107 (1997) · Zbl 0865.68046
[10] A. Finkel, G. Sutre, Decidability of reachability problems for classes of two counter automata, Proc. 17th Internat. Conf. on Theoretical Aspects of Computer Science (STACS 2000), Lecture Notes in Computer Science, Vol. 1770, Springer, Berlin, 2000, pp. 346-357.; A. Finkel, G. Sutre, Decidability of reachability problems for classes of two counter automata, Proc. 17th Internat. Conf. on Theoretical Aspects of Computer Science (STACS 2000), Lecture Notes in Computer Science, Vol. 1770, Springer, Berlin, 2000, pp. 346-357. · Zbl 0953.03050
[11] Ginsburg, S.; Spanier, E., Bounded Algol-like languages, Trans. Amer. Math. Soc., 113, 333-368 (1964) · Zbl 0142.24803
[12] Gurari, E. M.; Ibarra, O. H., An NP-complete number-theoretic problem, J. ACM, 26, 567-581 (1979) · Zbl 0407.68053
[13] Gurari, E. M.; Ibarra, O. H., Simple counter machines and number-theoretic problems, J. Comput. System Sci., 19, 145-162 (1979) · Zbl 0426.68036
[14] Ibarra, O. H., Reversal-bounded multicounter machines and their decision problems, J. ACM, 25, 116-133 (1978) · Zbl 0365.68059
[15] Ibarra, O. H.; Jiang, T.; Tran, N.; Wang, H., New decidability results concerning two-way counter machines, SIAM J. Comput., 24, 1, 123-137 (1995) · Zbl 0828.68075
[16] O.H. Ibarra, J. Su, Z. Dang, T. Bultan, R.A. Kemmerer, Counter machines: decidable properties and applications to verification problems, Proc. 25th Internat. Conf. on Mathematical Foundations of Computer Science (MFCS 2000), Lecture Notes in Computer Science, Vol. 1893, Springer, Berlin, 1998, pp. 426-435.; O.H. Ibarra, J. Su, Z. Dang, T. Bultan, R.A. Kemmerer, Counter machines: decidable properties and applications to verification problems, Proc. 25th Internat. Conf. on Mathematical Foundations of Computer Science (MFCS 2000), Lecture Notes in Computer Science, Vol. 1893, Springer, Berlin, 1998, pp. 426-435. · Zbl 0996.68091
[17] Matijasevic, Y., Enumerable sets are Diophantine, Soviet Math. Dokl, 11, 354-357 (1970)
[18] K.L. McMillan, Symbolic model-checking—an approach to the state explosion problem, Ph.D. Thesis, Department of Computer Science, Carnegie Mellon University, 1992.; K.L. McMillan, Symbolic model-checking—an approach to the state explosion problem, Ph.D. Thesis, Department of Computer Science, Carnegie Mellon University, 1992.
[19] Minsky, M., Recursive unsolvability of Post’s problem of Tag and other topics in the theory of Turing machines, Ann. Math., 74, 437-455 (1961) · Zbl 0105.00802
[20] Parikh, R., On context-free languages, J. ACM, 13, 570-581 (1966) · Zbl 0154.25801
[21] Peng, W.; Purushothaman, S., Analysis of a class of communicating finite state machines, Acta Inform., 29, 6/7, 499-522 (1992) · Zbl 0790.68042
[22] Valiant, L. G.; Paterson, M. S., Deterministic one-counter automata, J. Comput. System Sci., 10, 340-350 (1975) · Zbl 0307.68038
[23] P. Wolper, B. Boigelot, Verifying systems with infinite but regular state spaces, in: Proc. 10th Internat. Conf. on Computer Aided Verification (CAV 1998), Lecture Notes in Computer Science, Vol. 1427, Springer, Berlin, 1998, pp. 88-97.; P. Wolper, B. Boigelot, Verifying systems with infinite but regular state spaces, in: Proc. 10th Internat. Conf. on Computer Aided Verification (CAV 1998), Lecture Notes in Computer Science, Vol. 1427, Springer, Berlin, 1998, pp. 88-97.
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.