×

Verification of qualitative \(\mathbb Z\) constraints. (English) Zbl 1157.68048

Summary: We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in \(\mathbb Z\). The constraint language includes periodicity constraints and comparison constraints of the form \(x=y\) and \(x<y\); it is closed under Boolean operations and admits a restricted form of existential quantification. Such constraints are used, for instance, in calendar formalisms or abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. This is the largest set of qualitative constraints over \(\mathbb Z\) known so far, shown to admit a decidable LTL extension.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q25 Analysis of algorithms and problem complexity

Software:

FAST
Full Text: DOI

References:

[1] Alur, R.; Dill, D., A theory of timed automata, Theoretical Computer Science, 126, 183-235 (1994) · Zbl 0803.68071
[2] Alur, R.; Henzinger, Th., A really temporal logic, Journal of the Association for Computing Machinery, 41, 1, 181-204 (1994) · Zbl 0807.68065
[3] Bertino, E.; Bettini, C.; Ferrari, E.; Samarati, P., An access control model supporting periodicity constraints and temporal reasoning, ACM Transactions on Databases Systems, 23, 3, 231-285 (1998)
[4] Bouajjani, A.; Bozga, M.; Habermehl, P.; Iosif, R.; Moro, P.; Vojnar, T., Programs with lists are counter automata, (CAV’06. CAV’06, Lecture Notes in Computer Science, vol. 4144 (2006), Springer), 517-531 · Zbl 1188.68181
[5] Balbiani, Ph.; Condotta, J. F., Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning, (FroCoS’02. FroCoS’02, Lecture Notes in Artificial Intelligence, vol. 2309 (2002), Springer), 162-173 · Zbl 1057.68116
[6] Balcázar, J.; Díaz, J.; Gabarró, J., Structural Complexity I (1988), Springer: Springer Berlin · Zbl 0638.68040
[7] A. Bouajjani, R. Echahed, P. Habermehl, On the verification problem of nonregular properties for nonregular processes, in: LICS’95, 1995, pp. 123-133; A. Bouajjani, R. Echahed, P. Habermehl, On the verification problem of nonregular properties for nonregular processes, in: LICS’95, 1995, pp. 123-133
[8] Bouajjani, A.; Esparza, J.; Maler, O., Reachability analysis of pushdown automata: Application to model-checking, (CONCUR’97. CONCUR’97, Lecture Notes in Computer Science, vol. 1243 (1997), Springer), 135-150 · Zbl 1512.68135
[9] Bérard, B., Untiming timed languages, Information Processing Letters, 55, 129-135 (1995) · Zbl 1004.68532
[10] Bardin, S.; Finkel, A.; Leroux, J.; Petrucci, L., Fast: Fast acceleration of symbolic transition systems, (CAV’03. CAV’03, Lecture Notes in Computer Science, vol. 2725 (2003), Springer), 118-121
[11] S. Bardin, A. Finkel, E. Lozes, A. Sangnier, From pointer systems to counter systems using shape analysis, in: AVIS’06, 2006; S. Bardin, A. Finkel, E. Lozes, A. Sangnier, From pointer systems to counter systems using shape analysis, in: AVIS’06, 2006
[12] Bozzelli, L.; Gascon, R., Branching-time temporal logic extended with presburger constraints, (LPAR’06. LPAR’06, Lecture Notes in Computer Science, vol. 4246 (2006), Springer), 197-211 · Zbl 1165.03324
[13] F. Baader, P. Hanschke, A scheme for integrating concrete domains into concept languages, in: IJCAI’91, 1991, pp. 452-457; F. Baader, P. Hanschke, A scheme for integrating concrete domains into concept languages, in: IJCAI’91, 1991, pp. 452-457 · Zbl 0742.68063
[14] Bozga, M.; Iosif, R.; Lakhnech, Y., Flat parametric counter automata, (ICALP’06. ICALP’06, Lecture Notes in Computer Science, vol. 4052 (2006), Springer), 577-588 · Zbl 1134.68028
[15] B. Boigelot, Symbolic methods for exploring infinite state spaces, Ph.D. Thesis, Université de Liège, 1998; B. Boigelot, Symbolic methods for exploring infinite state spaces, Ph.D. Thesis, Université de Liège, 1998
[16] Caucal, D., On infinite transition graphs having a decidable monadic theory, Theoretical Computer Science, 290, 79-115 (2003) · Zbl 1019.68066
[17] Comon, H.; Cortier, V., Flatness is not a weakness, (CSL’00. CSL’00, Lecture Notes in Computer Science, vol. 1862 (2000), Springer), 262-276 · Zbl 0973.68142
[18] Čera¯ns, K., Deciding properties of integral relational automata, (ICALP. ICALP, Lecture Notes in Computer Science, vol. 820 (1994), Springer), 35-46 · Zbl 1418.68126
[19] Clarke, E.; Grumberg, O.; Long, D., Model checking and abstraction, ACM Transactions on Programming Languages and Systems, 16, 5, 1512-1542 (1994)
[20] Comon, H.; Jurski, Y., Multiple counters automata, safety analysis and Presburger arithmetic, (CAV’98. CAV’98, Lecture Notes in Computer Science, vol. 1427 (1998), Springer), 268-279
[21] A. Chandra, P. Merlin, Optimal implementation of conjunctive queries in relational databases, in: 9th ACM Symposium on Theory of Computing, 1977, pp. 77-90; A. Chandra, P. Merlin, Optimal implementation of conjunctive queries in relational databases, in: 9th ACM Symposium on Theory of Computing, 1977, pp. 77-90
[22] Demri, S.; D’Souza, D., An automata-theoretic approach to constraint LTL, Information and Computation, 205, 3, 380-415 (2007) · Zbl 1113.03015
[23] Demri, S., LTL over integer periodicity constraints, Theoretical Computer Science, 360, 1-3, 96-123 (2006) · Zbl 1097.68073
[24] Demri, S.; Finkel, A.; Goranko, V.; van Drimmelen, G., Towards a model-checker for counter systems, (Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis. Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, ATVA’06. Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis. Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, ATVA’06, Lecture Notes in Computer Science, vol. 4218 (2006), Springer), 493-507 · Zbl 1161.68563
[25] Demri, S.; Gascon, R., Verification of qualitative \(Z\)-constraints, (Proceedings of the 16th International Conference on Concurrency Theory. Proceedings of the 16th International Conference on Concurrency Theory, CONCUR’05. Proceedings of the 16th International Conference on Concurrency Theory. Proceedings of the 16th International Conference on Concurrency Theory, CONCUR’05, Lecture Notes in Computer Science, vol. 3653 (August 2005), Springer), 518-532 · Zbl 1134.68405
[26] Dang, Z.; Ibarra, O. H., The existence of \(\omega \)-chains for transitive mixed linear relations and its applications, International Journal of Foundations of Computer Science, 13, 6, 911-936 (2002) · Zbl 1067.68090
[27] Dang, Z.; San Pietro, P.; Kemmerer, R. A., Presburger liveness verification of discrete timed automata, Theoretical Computer Science, 1-3, 299, 413-438 (2003) · Zbl 1040.68050
[28] J. Esparza, A. Finkel, R. Mayr, On the verification of broadcast protocols, in: LICS’99, 1999, pp. 352-359; J. Esparza, A. Finkel, R. Mayr, On the verification of broadcast protocols, in: LICS’99, 1999, pp. 352-359
[29] Finkel, A.; Leroux, J., How to compose Presburger accelerations: Applications to broadcast protocols, (FST&TCS’02. FST&TCS’02, Lecture Notes in Computer Science, vol. 2256 (2002), Springer), 145-156 · Zbl 1027.68616
[30] Finkel, A.; Sutre, G., Decidability of reachability problems for classes of two counters automata, (STACS’00. STACS’00, Lecture Notes in Computer Science, vol. 2256 (2000), Springer), 346-357 · Zbl 0953.03050
[31] R. Gascon, Spécification et vérification de propriétés quantitatives sur des automates à contraintes, Ph.D. Thesis, ENS de Cachan, November 2007; R. Gascon, Spécification et vérification de propriétés quantitatives sur des automates à contraintes, Ph.D. Thesis, ENS de Cachan, November 2007
[32] Gastin, P.; Kuske, D., Satisfiability and model checking for MSO-definable temporal logics are in PSPACE, (CONCUR’03. CONCUR’03, Lecture Notes in Computer Science, vol. 2761 (2003), Springer), 222-236 · Zbl 1195.68068
[33] D. Gabelaia, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev, On the computational complexity of spatio-temporal logics, in: FLAIRS’03, 2003, pp. 460-464; D. Gabelaia, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev, On the computational complexity of spatio-temporal logics, in: FLAIRS’03, 2003, pp. 460-464 · Zbl 1080.68682
[34] Harel, E.; Lichtenstein, O.; Pnueli, A., Explicit clock temporal logic, (Proc. 5th IEEE Symp. Logic in Computer Science. Proc. 5th IEEE Symp. Logic in Computer Science, LICS ’90, Philadelphia, PA, USA, June 1990 (1990), IEEE Computer Society Press), 400-413 · Zbl 0825.68599
[35] Henzinger, Th.; Majumdar, R.; Raskin, J. F., A classification of symbolic transitions systems, ACM Transactions on Computational Logic, 6, 1, 1-32 (2005) · Zbl 1367.68193
[36] Ibarra, O., Reversal-bounded multicounter machines and their decision problems, Journal of the Association for Computing Machinery, 25, 1, 116-133 (1978) · Zbl 0365.68059
[37] Ibarra, O.; Dang, Z., On removing the stack from reachability constructions, (ISAAC’01. ISAAC’01, Lecture Notes in Computer Science, vol. 2223 (2001), Springer), 244-256 · Zbl 1077.68668
[38] Jančar, P.; Kučera, A.; Moller, F.; Sawa, Z., DP lower bounds for equivalence-checking and model-checking of one-counter automata, Information and Computation, 1, 188, 1-19 (2004) · Zbl 1078.68087
[39] Dal Lago, U.; Montanari, A., Calendars, time granularities, and automata, (Int. Symposium on Spatial and Temporal Databases. Int. Symposium on Spatial and Temporal Databases, Lecture Notes in Computer Science, vol. 2121 (2001), Springer: Springer Berlin), 279-298 · Zbl 0997.68567
[40] Logothetis, G.; Schneider, K., Abstraction from counters: an application on real-time systems, (TIME’01 (2001), IEEE), 214-223
[41] Lutz, C., NEXPTIME-complete description logics with concrete domains, ACM Transactions on Computational Logic, 5, 4, 669-705 (2004) · Zbl 1367.68288
[42] Minsky, M., Computation, Finite and Infinite Machines (1967), Prentice Hall · Zbl 0195.02402
[43] Müller-Olm, M.; Seidl, H., Analysis of modular arithmetic, (ESOP’05. ESOP’05, Lecture Notes in Computer Science, vol. 3444 (2005), Springer), 46-60 · Zbl 1108.68404
[44] Muller, D.; Schupp, P., The theory of ends, pushdown automata, and second-order logic, Theoretical Computer Science, 37, 51-75 (1985) · Zbl 0605.03005
[45] G. Puppis, Automata for Branching and Layered Temporal Structures, Ph.D. Thesis, University of Udine, 2006; G. Puppis, Automata for Branching and Layered Temporal Structures, Ph.D. Thesis, University of Udine, 2006 · Zbl 1181.03044
[46] Revesz, P., Introduction to Constraint Databases (2002), Springer: Springer New York · Zbl 0995.68035
[47] S. Safra, On the complexity of \(\omega \); S. Safra, On the complexity of \(\omega \)
[48] Sistla, A.; Clarke, E., The complexity of propositional linear temporal logic, Journal of the Association for Computing Machinery, 32, 3, 733-749 (1985) · Zbl 0632.68034
[49] Vardi, M.; Wolper, P., Reasoning about infinite computations, Information and Computation, 115, 1-37 (1994) · Zbl 0827.03009
[50] Wolper, P., Temporal logic can be more expressive, Information and Computation, 56, 72-99 (1983) · Zbl 0534.03009
[51] F. Wolter, M. Zakharyaschev, Spatio-temporal representation and reasoning based on RCC-8, in: KR’00, 2000, pp. 3-14; F. Wolter, M. Zakharyaschev, Spatio-temporal representation and reasoning based on RCC-8, in: KR’00, 2000, pp. 3-14
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.