×

zbMATH — the first resource for mathematics

The complexity of reversal-bounded model-checking. (English) Zbl 1348.68121
Tinelli, Cesare (ed.) et al., Frontiers of combining systems. 8th international symposium, FroCoS 2011, Saarbrücken, Germany, October 5–7, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24363-9/pbk). Lecture Notes in Computer Science 6989. Lecture Notes in Artificial Intelligence, 71-86 (2011).
Summary: We study model-checking problems on counter systems when guards are quantifier-free Presburger formulae, the specification languages are LTL-like dialects with arithmetical constraints and the runs are restricted to reversal-bounded ones. We introduce a generalization of reversal-boundedness and we show the NExpTime-completeness of the reversal-bounded model-checking problem as well as for related reversal-bounded reachability problems. As a by-product, we show the effective Presburger definability for sets of configurations for which there is a reversal-bounded run verifying a given temporal formula. Our results generalize existing results about reversal-bounded counter automata and provides a uniform and more general framework.
For the entire collection see [Zbl 1223.68012].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q25 Analysis of algorithms and problem complexity
Software:
cvc3; TaPAS; z3; LIRA
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R., Henzinger, T.: A really temporal logic. In: FOCS 1989, pp. 164–169. IEEE, Los Alamitos (1989) · Zbl 0807.68065
[2] Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007) · Zbl 05216239
[3] Becker, B., Dax, C., Eisinger, J., Klaedtke, F.: LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 307–310. Springer, Heidelberg (2007) · Zbl 05216241
[4] Bersani, M., Demri, S.: The complexity of reversal-bounded model checking. Tech. Rep. LSV-11-10, LSV, ENS Cachan, France (May 2011) · Zbl 1348.68121
[5] Bersani, M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: TIME 2010, pp. 43–50. IEEE, Los Alamitos (2010)
[6] Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)
[7] Borosh, I., Treybig, L.: Bounds on positive integral solutions of linear diophantine equations. Proocedings of The American Mathematical Society 55, 299–304 (1976) · Zbl 0291.10014
[8] Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: LICS 1995, pp. 123–133 (1995)
[9] Čerāns, K.: Deciding properties of integral relational automata. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol. 820, pp. 35–46. Springer, Heidelberg (1994)
[10] Dang, Z., Ibarra, O., San Pietro, P.: Liveness verification of reversal-bounded multicounter machines with a free counter. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 132–143. Springer, Heidelberg (2001) · Zbl 1053.03021
[11] Demri, S.: On Selective Unboundedness of VASS. In: INFINITY 2010. EPTCS, vol. 39, pp. 1–15 (2010)
[12] Esparza, J.: Decidability and complexity of Petri net problems – an introduction. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998) · Zbl 0926.68087
[13] Finkel, A., Sangnier, A.: Reversal-bounded counter machines revisited. In: Ochmański, E., Tyszkiewicz, J. (eds.) MFCS 2008. LNCS, vol. 5162, pp. 323–334. Springer, Heidelberg (2008) · Zbl 1173.68562
[14] Gurari, E., Ibarra, O.: The complexity of decision problems for finite-turn multicounter machines. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 495–505. Springer, Heidelberg (1981) · Zbl 0458.68011
[15] Habermehl, P.: On the complexity of the linear-time mu-calculus for Petri nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 102–116. Springer, Heidelberg (1997)
[16] Hague, M., Lin, A.W.: Model checking recursive programs with numeric data types. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 743–759. Springer, Heidelberg (2011) · Zbl 05940758
[17] Howell, R., Rosier, L.: An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines. JCSS 34(1), 55–74 (1987) · Zbl 0629.68054
[18] Ibarra, O.H., Bultan, T., Su, J.: Reachability analysis for some models of infinite-state transition systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 183–198. Springer, Heidelberg (2000) · Zbl 0999.68139
[19] Ibarra, O., Su, J., Dang, Z., Bultan, T., Kemmerer, R.: Counter Machines and Verification Problems. TCS 289(1), 165–189 (2002) · Zbl 1061.68095
[20] Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. JACM 25(1), 116–133 (1978) · Zbl 0365.68059
[21] Kopczynski, E., To, A.: Parikh Images of Grammars: Complexity and Applications. In: LICS 2010, pp. 80–89. IEEE, Los Alamitos (2010)
[22] Laroussinie, F., Meyer, A., Petonnet, E.: Counting LTL. In: TIME 2010, pp. 51–58. IEEE, Los Alamitos (2010)
[23] Leroux, J., Point, G.: TaPAS: The Talence Presburger Arithmetic Suite. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 182–185. Springer, Heidelberg (2009) · Zbl 1234.03002
[24] Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 489–503. Springer, Heidelberg (2005) · Zbl 1170.68519
[25] Lutz, C.: NEXPTIME-complete description logics with concrete domains. ACM ToCL 5(4), 669–705 (2004) · Zbl 1367.68288
[26] de Moura, L., Björner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · Zbl 05262379
[27] Papadimitriou, C.: On the complexity of integer programming. JACM 28(4), 765–768 (1981) · Zbl 0468.68050
[28] Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier congrès de mathématiciens des Pays Slaves, Warszawa, pp. 92–101 (1930)
[29] Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005) · Zbl 1087.68598
[30] Rackoff, C.: The covering and boundedness problems for vector addition systems. TCS 6(2), 223–231 (1978) · Zbl 0368.68054
[31] Suzuki, N., Jefferson, D.: Verification Decidability of Presburger Array Programs. JACM 27(1), 191–205 (1980) · Zbl 0429.68025
[32] To, A.: Model Checking Infinite-State Systems: Generic and Specific Approaches. Ph.D. thesis, School of Informatics, University of Edinburgh (2010)
[33] To, A., Libkin, L.: Algorithmic metatheorems for decidable LTL model checking over infinite systems. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 221–236. Springer, Heidelberg (2010) · Zbl 1284.68416
[34] Vardi, M., Wolper, P.: Reasoning about infinite computations. I&C 115, 1–37 (1994) · Zbl 0827.03009
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.