×
Bollig, Benedikt; Kuske, Dietrich; Mennicke, Roy

The complexity of model checking multi-stack systems. (English) Zbl 1366.68164

Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25–28, 2013. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-5020-6). 163-172 (2013).

Cited in 1 Review
Cited in 3 Documents

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

temporal logics; nested words; model checking; satisfiability problem

Citations:

Zbl 0921.03023
Cite Review PDF
Full Text: DOI

References:

[1] R. Alur, M. Arenas, P. Barcelo, K. Etessami, N. Immerman, and L. Libkin, “First-order and temporal logics for nested words,” Logical Methods in Computer Science, vol. 4, no. 11, pp. 1-44, 2008. · Zbl 1159.03018
[2] R. Alur, K. Etessami, and P. Madhusudan, “A temporal logic of nested calls and returns,” in Proceedings of TACAS 2004, LNCS, vol. 2988. Springer, 2004, pp. 467-481. · Zbl 1126.68466
[3] R. Alur and P. Madhusudan, “Adding nesting structure to words,” Journal of the ACM, vol. 56, pp. 16:1-16:43, 2009. · Zbl 1325.68138
[4] M. F. Atig, “Global Model Checking of Ordered Multi-Pushdown Systems,” in Proceedings of FSTTCS 2010, ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 8, 2010, pp. 216-227. · Zbl 1245.68130
[5] M. F. Atig, B. Bollig, and P. Habermehl, “Emptiness of multi-pushdown automata is 2ETIME-complete,” in Proceedings of DLT 2008, LNCS, vol. 5257. Springer, 2008, pp. 121-133. · Zbl 1161.68509
[6] M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan, “Linear-time model-checking for multithreaded programs under scope-bounding,” in Proceedings of ATVA’12, M. Mukund and S. Chakraborty, Eds., vol. 7561. Springer, Oct. 2012, pp. 152-166. · Zbl 1375.68076
[7] M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan, “Model checking branching-time properties of multi-pushdown systems is hard,” CoRR, vol. abs/1205.6928, 2012.
[8] B. Bollig, A. Cyriac, P. Gastin, and M. Zeitoun, “Temporal logics for concurrent recursive programs: Satisfiability and model checking,” in Proceedings of MFCS’11, LNCS, vol. 6907. Springer, 2011, pp. 132- 144. · Zbl 1343.68055
[9] L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi Reghizzi, “Multipush-down languages and grammars,” International Journal of Foundations of Computer Science, vol. 7, no. 3, pp. 253-292, 1996. · Zbl 0859.68053
[10] A. Cyriac, P. Gastin, and K. Narayan Kumar, “MSO decidability of multi-pushdown systems via split-width,” in Proceedings of CONCUR 2012, LNCS, vol. 7454. Springer, 2012, pp. 547-561. · Zbl 1364.68280
[11] R. Fagin, L. Stockmeyer, and M. Vardi, “On monadic NP vs. monadic co-NP (extended abstract),” in Structure in Complexity Theory Conference, 1993, pp. 19-30.
[12] D. Gabbay, I. Hodkinson, and M. Reynolds, Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Oxford University Press, 1994. · Zbl 0921.03023
[13] P. Gastin and D. Kuske, “Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces,” Information and Computation, vol. 208, no. 7, pp. 797-816, 2010. · Zbl 1195.68069
[14] S. Göller and A. W. Lin, “Concurrency Makes Simple Theories Hard,” in Proceedings of STACS’12, ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 14, 2012, pp. 148-159. · Zbl 1245.68136
[15] W. Hanf, “Model-theoretic methods in the study of elementary logic,” in The Theory of Models, J. Addison, L. Henkin, and A. Tarski, Eds. North Holland, 1965, pp. 132-145. · Zbl 0166.25801
[16] A. Heußner, J. Leroux, A. Muscholl, and G. Sutre, “Reachability analysis of communicating pushdown systems,” Logical Methods in Computer Science, vol. 8, no. 3:23, pp. 1-20, 2012. · Zbl 1248.68330
[17] S. La Torre, P. Madhusudan, and G. Parlato, “A robust class of context-sensitive languages,” in Proceedings of LICS’07. IEEE Computer Society Press, 2007, pp. 161-170.
[18] S. La Torre, P. Madhusudan, and G. Parlato, “Context-bounded analysis of concurrent queue systems,” in Proceedings of TACAS 2008, LNCS. Springer, 2008, pp. 299-314. · Zbl 1134.68446
[19] S. La Torre, P. Madhusudan, and G. Parlato, “An infinite automaton characterization of double exponential time,” in Proceedings of CSL’08, LNCS, vol. 5213. Springer-Verlag, 2008. · Zbl 1157.68040
[20] S. La Torre and M. Napoli, “Reachability of multistack pushdown systems with scope-bounded matching relations,” in Proceedings of CONCUR 2011, LNCS, vol. 6901. Springer, 2011, pp. 203-218. · Zbl 1343.68172
[21] S. La Torre and M. Napoli, “A temporal logic for multi-threaded programs,” in Proceedings of IFIP-TCS’12, LNCS. Springer, 2012, vol. 7604, pp. 225-239. · Zbl 1362.68051
[22] S. La Torre and G. Parlato, “Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width,” in Proceedings of FSTTCS 2012, ser. Leibniz International Proceedings in Informatics (LIPIcs), D. D’Souza, T. Kavitha, and J. Radhakrishnan, Eds., vol. 18, 2012, pp. 173-184. · Zbl 1354.68198
[23] P. Madhusudan and G. Parlato, “The tree width of auxiliary storage,” in Proceedings of POPL 2011. ACM, 2011, pp. 283-294. · Zbl 1284.68358
[24] O. Matz and W. Thomas, “The monadic quantifier alternation hierarchy over graphs is infinite,” in LICS’97. IEEE Computer Society Press, 1997, pp. 236-244.
[25] A. Pnueli, “The temporal logic of programs,” in Proceedings of FOCS 1977. IEEE, 1977, pp. 46-57.
[26] S. Qadeer and J. Rehof, “Context-bounded model checking of concurrent software,” in Proceedings of TACAS 2005, LNCS, vol. 3440. Springer, 2005, pp. 93-107. · Zbl 1087.68598
[27] K. Reinhardt, “The complexity of translating logic to finite automata,” in Automata Logics, and Infinite Games, LNCS, E. Grädel, W. Thomas, and T. Wilke, Eds. Springer, 2002, vol. 2500, pp. 231-238. · Zbl 1021.03031
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.