Equivalence between model-checking flat counter systems and Presburger arithmetic. (English) Zbl 1393.68101
Ouaknine, Joël (ed.) et al., Reachability problems. 8th international workshop, RP 2014, Oxford, UK, September 22–24, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-11438-5/pbk). Lecture Notes in Computer Science 8762, 85-97 (2014).
Summary: We show that model-checking flat counter systems over CTL* (with arithmetical constraints on counter values) has the same complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with the temporal operator EF only, no arithmetical constraints in the logical language and with guards on transitions made of simple linear constraints. This 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.
For the entire collection see [Zbl 1317.68013].
For the entire collection see [Zbl 1317.68013].
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] | Berman, L., The complexity of logical theories, TCS, 11, 71-78 (1980) · Zbl 0475.03017 · doi:10.1016/0304-3975(80)90037-7 |
| [2] | Bersani, M.; Demri, S.; Tinelli, C.; Sofronie-Stokkermans, V., The complexity of reversal-bounded model-checking, Frontiers of Combining Systems, 71-86 (2011), Heidelberg: Springer, Heidelberg · Zbl 1348.68121 · doi:10.1007/978-3-642-24364-6_6 |
| [3] | Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Université de Liège (1998) |
| [4] | Bozga, M.; Iosif, R.; Konečný, F.; McMillan, K. L.; Rival, X., Safety problems are NP-complete for flat integer programs with octagonal loops, Verification, Model Checking, and Abstract Interpretation, 242-261 (2014), Heidelberg: Springer, Heidelberg · Zbl 1428.68160 · doi:10.1007/978-3-642-54013-4_14 |
| [5] | Bruyère, V.; Dall’Olio, E.; Raskin, J.; Alt, H.; Habib, M., Durations, parametric model-checking in timed automata with presburger arithmetic, STACS 2003, 687-698 (2003), Heidelberg: Springer, Heidelberg · Zbl 1035.68063 · doi:10.1007/3-540-36494-3_60 |
| [6] | Comon, H.; Jurski, Y.; Vardi, M. Y., Multiple counter automata, safety analysis and Presburger Arithmetic, Computer Aided Verification, 268-279 (1998), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0028751 |
| [7] | de Moura, L.; Bjørner, N. S.; Ramakrishnan, C. R.; Rehof, J., Z3: An efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24 |
| [8] | Demri, S.; Dhar, A. K.; Sangnier, A.; Gramlich, B.; Miller, D.; Sattler, U., Taming past LTL and flat counter systems, Automated Reasoning, 179-193 (2012), Heidelberg: Springer, Heidelberg · Zbl 1358.68186 · doi:10.1007/978-3-642-31365-3_16 |
| [9] | Demri, S.; Dhar, A. K.; Sangnier, A.; Fomin, F. V.; Freivalds, R.; Kwiatkowska, M.; Peleg, D., On the complexity of verifying regular properties on flat counter systems,, Automata, Languages, and Programming, 162-173 (2013), Heidelberg: Springer, Heidelberg · Zbl 1334.68130 · doi:10.1007/978-3-642-39212-2_17 |
| [10] | Demri, S.; Finkel, A.; Goranko, V.; van Drimmelen, G., Model-checking CTL^* over flat Presburger counter systems, JANCL, 20, 4, 313-344 (2010) · Zbl 1242.68157 |
| [11] | Dhar, A.K.: Applying Satisfiability Modulo Theories Techniques to the Verification of Infinite-State Systems. PhD thesis, Université Paris VII-Denis Diderot (2014) |
| [12] | Emerson, A.; Halpern, J., ‘sometimes‘ and ’not never’ revisited: on branching versus linear time temporal logic, JACM, 33, 151-178 (1986) · Zbl 0629.68020 · doi:10.1145/4904.4999 |
| [13] | Emerson, E. A.; Lei, C.-L., Modalities for model checking: Branching time logic strikes back, Sci. Comput. Program., 8, 3, 275-306 (1987) · Zbl 0615.68019 · doi:10.1016/0167-6423(87)90036-0 |
| [14] | Finkel, A.; Leroux, J.; Agrawal, M.; Seth, A. K., How to compose presburger-accelerations: Applications to broadcast protocols, FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 145-156 (2002), Heidelberg: Springer, Heidelberg · Zbl 1027.68616 |
| [15] | Göller, S.; Haase, C.; Ouaknine, J.; Worrell, J.; Birkedal, L., Branching-time model checking of parametric one-counter automata, Foundations of Software Science and Computational Structures, 406-420 (2012), Heidelberg: Springer, Heidelberg · Zbl 1352.68153 · doi:10.1007/978-3-642-28729-9_27 |
| [16] | 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 · doi:10.1137/120876435 |
| [17] | Habermehl, P.; Azéma, P.; Balbo, G., On the complexity of the linear-time mu-calculus for Petri nets, Application and Theory of Petri Nets 1997, 102-116 (1997), Heidelberg: Springer, Heidelberg · Zbl 1523.68041 · doi:10.1007/3-540-63139-9_32 |
| [18] | Laroussinie, F.; Markey, N.; Schnoebelen, P.; Honsell, F.; Miculan, M., Model checking CTL^+ and FCTL is hard, Foundations of Software Science and Computation Structures, 318-331 (2001), Heidelberg: Springer, Heidelberg · Zbl 0986.68067 · doi:10.1007/3-540-45315-6_21 |
| [19] | Leroux, J.: Presburger counter machines. Habilitation thesis, U. of Bordeaux (2012) |
| [20] | Leroux, J.; Point, G.; Kowalewski, S.; Philippou, A., TaPAS: The talence presburger arithmetic suite, Tools and Algorithms for the Construction and Analysis of Systems, 182-185 (2009), Heidelberg: Springer, Heidelberg · Zbl 1234.03002 · doi:10.1007/978-3-642-00768-2_18 |
| [21] | Leroux, J.; Sutre, G.; Gardner, P.; Yoshida, N., On flatness for 2-dimensional vector addition systems with states, CONCUR 2004 - Concurrency Theory, 402-416 (2004), Heidelberg: Springer, Heidelberg · Zbl 1099.68071 · doi:10.1007/978-3-540-28644-8_26 |
| [22] | Leroux, J.; Sutre, G.; Peled, D. A.; Tsay, Y.-K., Flat counter automata almost everywhere?, Automated Technology for Verification and Analysis, 489-503 (2005), Heidelberg: Springer, Heidelberg · Zbl 1170.68519 · doi:10.1007/11562948_36 |
| [23] | Minsky, M., Computation, Finite and Infinite Machines (1967), Englewood Cliffs: Prentice-Hall, Englewood Cliffs · Zbl 0195.02402 |
| [24] | 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 (1929) · JFM 56.0825.04 |
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.
