The complexity of model checking multi-stack systems. (English) Zbl 1372.68164
Summary: We study the linear-time model checking problem for Boolean concurrent programs with recursive procedure calls. While sequential recursive programs are usually modeled as pushdown automata, concurrent recursive programs involve several processes and can be naturally abstracted as pushdown automata with multiple stacks. Their behavior can be understood as words with multiple nesting relations, each relation connecting a procedure call with its corresponding return. To reason about multiply nested words, we consider the class of all temporal logics as defined in the book by D. M. Gabbay et al. [Temporal logic. Vol. 1. Mathematical foundations and computational aspects. Oxford: Clarendon Press (1994; Zbl 0921.03023)]. The unifying feature of these temporal logics is that their modalities are defined in monadic second-order (MSO) logic. In particular, this captures numerous temporal logics over concurrent and/or recursive programs that have been defined so far. Since the general model checking problem is undecidable, we restrict attention to phase bounded executions as proposed by S. La Torre et al. [“A robust class of context-sensitive languages”, in: Proceedings of the 22nd annual IEEE symposium on logic in computer science, LICS’07. Los Alamitos, CA: IEEE Computer Society. 161–170 (2007; doi:10.1109/LICS.2007.9)]. While the MSO model checking problem in this case is non-elementary, our main result states that the model checking (and satisfiability) problem for all MSO-definable temporal logics is decidable in elementary time. More precisely, it is solvable in time exponential in the formula and \((n+2)\)-fold exponential in the number of phases where \(n\) is the maximal level of the MSO modalities in the monadic quantifier alternation hierarchy (which is a vast improvement over the conference version of this paper [in: Proceedings of the 28th annual ACM/IEEE symposium on logic in computer science, LICS’13. Los Alamitos, CA: IEEE Computer Society. 163–172 (2013; Zbl 1366.68164)] where the space was also \((n+2)\)-fold exponential in the size of the temporal formula). We complement this result and provide, for each level \(n\), a temporal logic whose model checking problem is \(n\)-EXPSPACE-hard.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Aiswarya, C., Gastin, P., Narayan Kumar, K.: Verifying communicating multi-pushdown systems via split-width. In: Proceedings of ATVA’14, pp 1-17 (2014) · Zbl 1448.68283 |
| [2] | Alur, R., Arenas, M., Barceló, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. Logical Methods Comput Sci 4(11), 1-44 (2008) · Zbl 1159.03018 |
| [3] | Alur, R., Etessami, K., Madhusudan, P.: A Temporal Logic of Nested Calls and Returns. In: Proceedings of TACAS’04, vol. 2988 of Lecture Notes in Computer Science, pp 467-481. Springer (2004) · Zbl 1126.68466 |
| [4] | Alur, R., Madhusudan, P.: Adding nesting structure to words. J ACM 56, 16:1-16:43 (2009) · Zbl 1325.68138 · doi:10.1145/1516512.1516518 |
| [5] | Atig, M.F.: Model-checking of ordered multi-pushdown automata. Logical Methods Comput Sci 8, 3 (2012) · Zbl 1279.68206 · doi:10.2168/LMCS-8(3:20)2012 |
| [6] | Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of multi-pushdown automata is 2ETIME-complete. In: Proceedings of DLT’08, vol. 5257 of Lecture Notes in Computer Science, pp 121-133. Springer (2008) · Zbl 1161.68509 |
| [7] | Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Linear-time model-checking for multithreaded programs under scope-bounding. In: Proceedings of ATVA’12, vol. 7561, pp 152-166. Springer (2012) · Zbl 1375.68076 |
| [8] | Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Model checking branching-time properties of multi-pushdown systems is hard (2012). CoRR, arXiv:1205.6928 · Zbl 1375.68076 |
| [9] | Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008) · Zbl 1179.68076 |
| [10] | Bollig, B., Cyriac, A., Gastin, P., Zeitoun, M.: Temporal logics for concurrent recursive programs: satisfiability and model checking. J. Applied Logic 12(4), 395-416 (2014) · Zbl 1310.68142 · doi:10.1016/j.jal.2014.05.001 |
| [11] | Bollig, B., Kuske, D.: An optimal construction of Hanf sentences. J. Appl. Log. 10(2), 179-186 (2012) · Zbl 1258.03048 · doi:10.1016/j.jal.2012.01.002 |
| [12] | Bollig, B., Kuske, D., Mennicke, R.: The complexity of model checking multi-stack systems. In: Proceedings of LICS’13, pp 163-172. IEEE Computer Society (2013) · Zbl 1366.68164 |
| [13] | Breveglieri, L., Cherubini, A., Citrini, C., Crespi Reghizzi, S.: Multi-push-down languages and grammars. Int. J. Found. Comput. Sci. 7(3), 253-292 (1996) · Zbl 0859.68053 · doi:10.1142/S0129054196000191 |
| [14] | Clarke, E. M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001) · Zbl 1423.68002 |
| [15] | Cyriac, A., Gastin, P., Narayan Kumar, K.: MSO decidability of multi-pushdown systems via split-width. In: Proceedings of CONCUR’12, volume 7454 of Lecture Notes in Computer Science, pp 547-561. Springer (2012) · Zbl 1364.68280 |
| [16] | Ebbinghaus, H.-D., Flum, J.: Finite model theory. Springer (1995) · Zbl 0841.03014 |
| [17] | Fagin, R., Stockmeyer, L.J., Vardi, M.: On monadic NP vs. monadic co-NP (Extended Abstract). In: Structure in complexity theory conference, pp 19-30. IEEE Computer Society Press (1993) · Zbl 0835.68046 |
| [18] | Gabbay, D.M., Hodkinson, I., Reynolds, M.A.: Temporal logic: Mathematical foundations and computational aspects, vol. 1. Oxford University Press (1994) · Zbl 0921.03023 |
| [19] | Gastin, P., Kuske, D.: Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. In: Proceedings of CONCUR’05 Lecture Notes in Comp. Science, vol. 3653, pp 533-547. Springer (2005) · Zbl 1134.68436 |
| [20] | Gastin, P., Kuske, D.: Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. Inf. Comput. 208(7), 797-816 (2010) · Zbl 1195.68069 · doi:10.1016/j.ic.2009.12.003 |
| [21] | Göller, S., Lin, A.W.: Concurrency makes simple theories hard. In: Proceedings of STACS’12, Volume 14 of Leibniz International Proceedings in Informatics (LIPIcs), pp 148-159 (2012) · Zbl 1245.68136 |
| [22] | Hanf, W.: Model-theoretic methods in the study of elementary logic. In: The theory of models, pp 132-145. North Holland (1965) · Zbl 0166.25801 |
| [23] | Heußner, A., Leroux, J., Muscholl, A., Sutre, G.: Reachability analysis of communicating pushdown systems. Logical Methods Comput Sci 8(3:23), 1-20 (2012) · Zbl 1248.68330 |
| [24] | La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: Proceedings of LICS’07, pp 161-170. IEEE Computer Society Press (2007) |
| [25] | La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Proceedings of TACAS’08 Lecture Notes in Computer Science, pp 299-314. Springer (2008) · Zbl 1134.68446 |
| [26] | La Torre, S., Madhusudan, P., Parlato, G.: An infinite automaton characterization of double exponential time. In: Proceedings of CSL’08, volume 5213 of Lecture Notes in Computer Science. Springer (2008) · Zbl 1157.68040 |
| [27] | La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: Proceedings of CONCUR 2011, volume 6901 of Lecture Notes in Computer Science, pp 203-218. Springer (2011) · Zbl 1343.68172 |
| [28] | La Torre, S., Napoli, M.: A temporal logic for multi-threaded programs. In: Proceedings of IFIP-TCS’12, Volume 7604 of Lecture Notes in Computer Science, pp 225-239. Springer (2012) · Zbl 1362.68051 |
| [29] | La Torre, S., Parlato, G.: Scope-bounded multistack pushdown systems: Fixed-point, sequentialization, and tree-width. In: Proceedings of FSTTCS’12, Volume 18 of Leibniz International Proceedings in Informatics (LIPIcs), pp 173-184 (2012) · Zbl 1354.68198 |
| [30] | Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: Proceedings of POPL’11, pp 283-294. ACM (2011) · Zbl 1284.68358 |
| [31] | Matz, O., Thomas, W.: The monadic quantifier alternation hierarchy over graphs is infinite. In: LICS’97, pp 236-244. IEEE Computer Society Press (1997) |
| [32] | Mennicke, R.: Model checking concurrent recursive programs using temporal logics. In: Proceedings of MFCS’14, Part I, volume 8634 of Lecture Notes in Computer Science, pp 438-450. Springer (2014) · Zbl 1425.68263 |
| [33] | Mennicke, R.: Model checking concurrent systems using temporal logics. PhD Thesis, Fakultät für Informatik und Automatisierung, Technische Universität Ilmenau (2015) · Zbl 1425.68263 |
| [34] | Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS’77, pp 46-57. IEEE (1977) · Zbl 1258.03048 |
| [35] | Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS’05, Volume 3440 of Lecture Notes in Computer Science, pp 93-107. Springer (2005) · Zbl 1087.68598 |
| [36] | Reinhardt, K.: The complexity of translating logic to finite automata. In: Automata, logics, and infinite games, volume 2500 of Lecture Notes in Computer Science, pp 231-238. Springer (2002) · Zbl 1021.03031 |
| [37] | Stockmeyer, L.: The complexity of decision problems in automata theory and logic. PhD thesis, MIT (1974) |
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.
