Equivalence between model-checking flat counter systems and Presburger arithmetic. (English) Zbl 1393.68100
Summary: We show that model-checking flat counter systems with the branching-time temporal logic CTL* extended with arithmetical constraints on counter values has the same worst-case complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with strong restrictions: the logical language uses only the temporal operator EF and no arithmetical constraints, and the guards on the transitions are made of linear constraints. This work complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL, for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 03F30 | First-order arithmetic and fragments |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
References:
| [1] | Barrett, C.; Conway, C.; Deters, M.; Hadarean, L.; Jovanovic, D.; King, T.; Reynolds, A.; Tinelli, C., CVC4, (CAV’11. CAV’11, Lecture Notes in Comput. Sci., vol. 8606 (2011), Springer), 171-177 |
| [2] | Berman, L., The complexity of logical theories, Theoret. Comput. Sci., 11, 71-78 (1980) · Zbl 0475.03017 |
| [3] | Bersani, M.; Demri, S., The complexity of reversal-bounded model-checking, (FROCOS’11. FROCOS’11, Lecture Notes in Artificial Intelligence, vol. 6989 (2011), Springer), 71-86 · Zbl 1348.68121 |
| [4] | Boigelot, B., Symbolic Methods for Exploring Infinite State Spaces (1998), Université de Liège, PhD thesis |
| [5] | Bozga, M.; Iosif, R.; Konecny, F., Safety problems are NP-complete for flat integer programs with octagonal loops, (VMCAI’14. VMCAI’14, Lecture Notes in Comput. Sci., vol. 8318 (2014), Springer), 242-261 · Zbl 1428.68160 |
| [6] | Bruyère, V.; Dall’Olio, E.; Raskin, J., Durations, parametric model-checking in timed automata with Presburger arithmetic, (STACS’03. STACS’03, Lecture Notes in Comput. Sci., vol. 2607 (2003), Springer), 687-698 · Zbl 1035.68063 |
| [7] | Comon, H.; Jurski, Y., Multiple counter automata, safety analysis and Presburger arithmetic, (CAV’98. CAV’98, Lecture Notes in Comput. Sci., vol. 1427 (1998), Springer), 268-279 |
| [8] | de Moura, L.; Björner, N., Z3: an efficient SMT solver, (TACAS’08. TACAS’08, Lecture Notes in Comput. Sci., vol. 4963 (2008), Springer), 337-340 |
| [9] | Demri, S.; Dhar, A.; Sangnier, A., Taming past LTL and flat counter systems, (IJCAR’12. IJCAR’12, Lecture Notes in Artificial Intelligence, vol. 7364 (2012), Springer), 179-193 · Zbl 1358.68186 |
| [10] | Demri, S.; Dhar, A.; Sangnier, A., On the complexity of verifying regular properties on flat counter systems, (ICALP’13. ICALP’13, Lecture Notes in Comput. Sci., vol. 7966 (2013), Springer), 162-173 · Zbl 1334.68130 |
| [11] | Demri, S.; Dhar, A.; Sangnier, A., Equivalence between model-checking flat counter systems and Presburger arithmetic, (RP’14. RP’14, Lecture Notes in Comput. Sci., vol. 8762 (2014), Springer), 85-97 · Zbl 1393.68101 |
| [12] | Demri, S.; Finkel, A.; Goranko, V.; van Drimmelen, G., Model-checking \(CTL^⁎\) over flat Presburger counter systems, J. Appl. Non-Classical Logics, 20, 4, 313-344 (2010) · Zbl 1242.68157 |
| [13] | Dhar, A., Algorithms for Model-Checking Flat Counter Systems (December 2014), Université Paris Diderot, PhD thesis |
| [14] | Emerson, E.; Halpern, J., ‘Sometimes’ and ‘not never’ revisited: on branching versus linear time temporal logic, J. ACM, 33, 151-178 (1986) · Zbl 0629.68020 |
| [15] | Emerson, E.; Lei, C.-L., Modalities for model checking: branching time logic strikes back, Sci. Comput. Program., 8, 3, 275-306 (1987) · Zbl 0615.68019 |
| [16] | Finkel, A.; Leroux, J., How to compose Presburger accelerations: applications to broadcast protocols, (FST&TCS’02. FST&TCS’02, Lecture Notes in Comput. Sci., vol. 2256 (2002), Springer), 145-156 · Zbl 1027.68616 |
| [17] | Fribourg, L.; Olsén, H., Proving safety properties of infinite state systems by compilation into Presburger arithmetic, (CONCUR’97. CONCUR’97, Lecture Notes in Comput. Sci., vol. 1243 (1997), Springer), 213-227 · Zbl 1512.68167 |
| [18] | Göller, S.; Haase, C.; Ouaknine, J.; Worrell, J., Branching-time model checking of parametric one-counter automata, (FoSSaCS’12. FoSSaCS’12, Lecture Notes in Comput. Sci., vol. 7213 (2012), Springer), 406-420 · Zbl 1352.68153 |
| [19] | Göller, S.; Lohrey, M., Branching-time model checking of one-counter processes and timed automata, SIAM J. Comput., 42, 3, 884-923 (2013) · Zbl 1275.68092 |
| [20] | Haase, C., Subclasses of Presburger arithmetic and the weak EXP hierarchy, (CSL-LICS’14 (2014), ACM), 47:1-47:10 · Zbl 1394.68153 |
| [21] | Haase, C.; Kreutzer, S.; Ouaknine, J.; Worrell, J., Reachability in succinct and parametric one-counter automata, (CONCUR’09. CONCUR’09, Lecture Notes in Comput. Sci., vol. 5710 (2009), Springer), 369-383 · Zbl 1254.68134 |
| [22] | Habermehl, P., On the complexity of the linear-time mu-calculus for Petri nets, (ICATPN’97. ICATPN’97, Lecture Notes in Comput. Sci., vol. 1248 (1997), Springer), 102-116 · Zbl 1523.68041 |
| [23] | Hague, M.; Lin, A. W., Model checking recursive programs numeric data types, (CAV’11. CAV’11, Lecture Notes in Comput. Sci., vol. 6806 (2011), Springer), 743-759 |
| [24] | Hemachandra, L., The strong exponential hierarchy collapses, J. Comput. System Sci., 39, 3, 299-322 (1989) · Zbl 0693.03022 |
| [25] | Ibarra, O., Reversal-bounded multicounter machines and their decision problems, J. ACM, 25, 116-133 (1978) · Zbl 0365.68059 |
| [26] | Kosaraju, S. R., Decidability of reachability in vector addition systems (preliminary version), (STOC’82 (1982)), 267-281 |
| [27] | Laroussinie, F.; Markey, N.; Schnoebelen, P., Model checking \(CTL^+\) and FCTL is hard, (FOSSACS’01. FOSSACS’01, Lecture Notes in Comput. Sci., vol. 2030 (2001), Springer), 318-331 · Zbl 0986.68067 |
| [28] | Lechner, A.; Mayr, R.; Ouaknine, J.; Pouly, A.; Worrell, J., Model checking flat freeze LTL on one-counter automata, (CONCUR’16. CONCUR’16, LIPIcs. Leibniz Int. Proc. Inform., vol. 59 (2016)), 29:1-29:14 · Zbl 1392.68257 |
| [29] | Leroux, J., Presburger Counter Machines (2012), U. of Bordeaux, Habilitation thesis |
| [30] | Leroux, J.; Point, G., TaPAS: the talence presburger arithmetic suite, (TACAS’09. TACAS’09, Lecture Notes in Comput. Sci., vol. 5505 (2009), Springer), 182-185 · Zbl 1234.03002 |
| [31] | Leroux, J.; Sutre, G., On flatness for 2-dimensional vector addition systems with states, (CONCUR. CONCUR, Lecture Notes in Comput. Sci., vol. 3170 (2004), Springer), 402-416 · Zbl 1099.68071 |
| [32] | Leroux, J.; Sutre, G., Flat counter automata almost everywhere!, (ATVA’05. ATVA’05, Lecture Notes in Comput. Sci., vol. 3707 (2005), Springer), 489-503 · Zbl 1170.68519 |
| [33] | Mayr, E., Persistence of vector replacement systems is decidable, Acta Inform., 15, 309-318 (1981) · Zbl 0454.68048 |
| [34] | Minsky, M., Computation, Finite and Infinite Machines (1967), Prentice Hall · Zbl 0195.02402 |
| [35] | Papadimitriou, C., Computational Complexity (1994), Addison-Wesley · Zbl 0833.68049 |
| [36] | Presburger, M., Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, (Comptes Rendus du premier congrès de mathématiciens des Pays Slaves. Comptes Rendus du premier congrès de mathématiciens des Pays Slaves, Warszawa (1929)), 92-101 · JFM 56.0825.04 |
| [37] | Suzuki, N.; Jefferson, D., Verification decidability of presburger array programs, J. ACM, 27, 1, 191-205 (1980) · Zbl 0429.68025 |
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.
