Abstract
We introduce some new models of infinite-state transition systems. The basic model, called a (reversal-bounded) counter machine (CM), is a nondeterministic finite automaton augmented with finitely many reversal-bounded counters (i.e. each counter can be incremented or decremented by 1 and tested for zero, but the number of times it can change mode from nondecreasing to nonincreasing and vice-versa is bounded by a constant, independent of the computation). We extend a CM by augmenting it with some familiar data structures: (i) A pushdown counter machine (PCM) is a CM augmented with an unrestricted pushdown stack. (ii) A tape counter machine (TCM) is a CM augmented with a two-way read/write worktape that is restricted in that the number of times the head crosses the boundary between any two adjacent cells of the worktape is bounded by a constant, independent of the computation (thus, the worktape is finite-crossing). There is no bound on how long the head can remain on a cell. (iii) A queue counter machine (QCM) is a CM augmented with a queue that is restricted in that the number of alternations between non-deletion phase and non-insertion phase is bounded by a constant. A non-deletion (non-insertion) phase is a period consisting of insertions (deletions) and no-changes, i.e., the queue is idle. We show that emptiness, (binary, forward, and backward) reachability, nonsafety, and invariance for these machines are solvable. We also look at extensions of the models that allow the use of linear-relation tests among the counters and parameterized constants as “primitive” predicates. We investigate the conditions under which these problems are still solvable.
Supported in part by NSF grants IRI-9700370 and IIS-9817432.
Supported in part by NSF grant CCR-9970976.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, C. Courcoibetis, and D. Dill. Model-checking in dense real time. Information & Computation, 104(1):2–34, 1993.
R. Alur and D. Dill. Automata for modeling real-time systems. Theoretical Computer Science, 126(2):183–236, 1994.
R. Alur and T. A. Henzinger. A really temporal logic. J. ACM, 41(1):181–204, 1994.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. H. Hwang. Symbolic model checking: 1020 states and beyond. Information & Computation, 98(2):142–170, June 1992.
A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model-Checking. CONCUR 1997, pp. 135–150.
A. Bouajjani, R. Echahed and R. Robbana. “On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures.” In Hybrid Systems II, LNCS 999, 1995.
B. Boigelot and P. Godefroid. “Symbolic verification of communication protocols with infinite state spaces using QDDs.” In Proc. Int. Conf. on Computer Aided Verification, 1996.
T. Bultan, R. Gerber, and W. Pugh. Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations, and Experimental Results. ACM Trans. on Programming Languages and Systems, 21(4):747–789, July 1999.
S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In Proc. 10th Int. Conf. on Computer Aided Verification, 1998.
B. Boigelot and P. Wolper, Symbolic verification with periodic sets, Proc. 6th Int. Conf. on Computer Aided Verification, 1994
H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. Proc. 10th Int. Conf. on Computer Aided Verification, 1998.
H. Comon and Y. Jurski. Timed Automata and the Theory of Real Numbers. Proc. CONCUR, 1999.
Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. Binary reachability analysis of discrete pushdown timed automata. To appear in Int. Conf. on Computer Aided Verification, 2000.
J. Dingel and T. Filkorn. Model checking for infinite state systems using data abstraction. Proc. 7th Int. Conf. on Computer Aided Verification, 1995.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. on Programming Languages and Systems, 19(2):253–291, March 1997.
J. Esparza. Decidability of Model Checking for Infinite-State Concurrent Systems. Acta Informatica, 34(2):85–107, 1997.
A. Finkel and G. Sutre. Decidability of reachability problems for classes of two counters automata. STACS’2000, 346–357, Springer, 2000.
A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. INFINITY, 1997.
E. M. Gurari and O. H. Ibarra. The complexity of decision problems for finite-turn multicounter machines. JCSS, 22:220–229, 1981.
S. A. Greibach. Checking automata and one-way stack languages. SDC Document TM 738/045/00, 1968.
T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-time Systems. Information & Computation, 111(2):193–244, 1994.
N. Halbwachs, P. Raymond, and Y. Proy. Verification of linear hybrid systems by means of convex approximations. In Proc. Int. Symposium on Static Analysis, B. LeCharlier ed., vol. 864, September 1994.
O. H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, Vol. 25, pp. 116–133, 1978.
O. H. Ibarra and J. Su, A Technique for the Containment and Equivalence of Linear Constraint Queries. JCSS, 59(1):1–28, 1999.
O. H. Ibarra, J. Su, and C. Bartzis, Counter Machines and the Safety and Disjointness Problems for Database Queries with Linear Constraints, to appear in Words, Sequences, Languages: Where Computer Science, Biology and Linguistics Meet, Kluwer, 2000.
O. H. Ibarra, J. Su, Z. Dang, T. Bultan, and R. Kemmerer, Counter Machines: Decidable Properties and Applications to Verification Problems, To appear in Proc. MFCS’2000.
Y. Matijasevic. Enumerable sets are Diophantine. Soviet Math. Dokl, Vol. 11, 1970, pp. 354–357.
M. Minsky. Recursive unsolvability of Post’s problem of Tag and other topics in the theory of Turing machines. Ann. of Math., 74:437–455, 1961.
E. Post. A variant of a recursively unsolvable problem. Bull. Am. Math. Soc., 52:264–268, 1946.
I. Walukiewicz. Pushdown processes: games and model checking. In Proc. Int. Conf. on Computer Aided Verification, 1996
P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In Proc. Int. Conf. on Computer Aided Verification, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ibarra, O.H., Bultan, T., Su, J. (2000). Reachability Analysis for Some Models of Infinite-State Transition Systems. In: Palamidessi, C. (eds) CONCUR 2000 — Concurrency Theory. CONCUR 2000. Lecture Notes in Computer Science, vol 1877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44618-4_15
Download citation
DOI: https://doi.org/10.1007/3-540-44618-4_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67897-7
Online ISBN: 978-3-540-44618-7
eBook Packages: Springer Book Archive