Temporal logics for concurrent recursive programs: satisfiability and model checking. (English) Zbl 1310.68142
Summary: We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and which, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Keywords:
temporal logic; concurrent recursive programs; nested words; Mazurkiewicz traces; satisfiability; model checkingReferences:
| [1] | Alur, R.; Madhusudan, P., Adding nesting structure to words, J. ACM, 56, 16:1-16:43 (2009) · Zbl 1325.68138 |
| [2] | Alur, R.; Etessami, K.; Madhusudan, P., A temporal logic of nested calls and returns, (TACAS’04. TACAS’04, Lect. Notes Comput. Sci., vol. 2988 (2004), Springer), 467-481 · Zbl 1126.68466 |
| [3] | Alur, R.; Arenas, M.; Barceló, P.; Etessami, K.; Immerman, N.; Libkin, L., First-order and temporal logics for nested words, Log. Methods Comput. Sci., 4, 11, 1-44 (2008) · Zbl 1159.03018 |
| [4] | Arora, S.; Barak, B., Computational Complexity: A Modern Approach (2009), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 1193.68112 |
| [5] | Atig, M. F., Global model checking of ordered multi-pushdown systems, (FSTTCS’10. FSTTCS’10, LIPIcs, vol. 8 (2010)), 216-227 · Zbl 1245.68130 |
| [6] | Atig, M. F.; Bollig, B.; Habermehl, P., Emptiness of multi-pushdown automata is 2ETIME-complete, (DLT’08. DLT’08, Lect. Notes Comput. Sci., vol. 5257 (2008), Springer), 121-133 · Zbl 1161.68509 |
| [7] | Bollig, B.; Grindei, M.-L.; Habermehl, P., Realizability of concurrent recursive programs, (FOSSACS’09. FOSSACS’09, Lect. Notes Comput. Sci., vol. 5504 (2009), Springer), 410-424 · Zbl 1234.68071 |
| [8] | Bollig, B.; Kuske, D.; Meinecke, I., Propositional dynamic logic for message-passing systems, Log. Methods Comput. Sci., 6, 3:16, 1-31 (2010) · Zbl 1201.03016 |
| [9] | Bollig, B.; Cyriac, A.; Gastin, P.; Zeitoun, M., Temporal logics for concurrent recursive programs: satisfiability and model checking, (MFCS’11. MFCS’11, Lect. Notes Comput. Sci., vol. 6907 (2011), Springer), 132-144 · Zbl 1343.68055 |
| [10] | Brand, D.; Zafiropulo, P., On communicating finite-state machines, J. ACM, 30, 2, 323-342 (1983) · Zbl 0512.68039 |
| [11] | 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 |
| [12] | Calvanese, D.; De Giacomo, G.; Lenzerini, M.; Vardi, M., An automata-theoretic approach to regular XPath, (DBPL’09. DBPL’09, Lect. Notes Comput. Sci., vol. 5708 (2009)), 18-35 |
| [13] | Clarke, E. M.; Emerson, E. A., Design and synthesis of synchronization skeletons using branching-time temporal logic, (Logic of Programs (1981)), 52-71 · Zbl 0546.68014 |
| [14] | Cyriac, A.; Gastin, P.; Narayan Kumar, K., MSO decidability of multi-pushdown systems via split-width, (CONCUR’12. CONCUR’12, Lect. Notes Comput. Sci., vol. 7454 (2012), Springer), 547-561 · Zbl 1364.68280 |
| [15] | Dax, C.; Klaedtke, F., Alternation elimination for automata over nested words, (FOSSACS’11. FOSSACS’11, Lect. Notes Comput. Sci. (2011), Springer), 168-183 · Zbl 1326.68175 |
| [16] | Diekert, V.; Gastin, P., Pure future local temporal logics are expressively complete for Mazurkiewicz traces, Inf. Comput., 204, 11, 1597-1619 (2006) · Zbl 1113.03016 |
| [17] | (Diekert, V.; Rozenberg, G., The Book of Traces (1995), World Scientific: World Scientific Singapore) |
| [18] | Fischer, M.; Ladner, R., Propositional dynamic logic of regular programs, J. Comput. Syst. Sci., 18, 2, 194-211 (1979) · Zbl 0408.03014 |
| [19] | Gastin, P.; Kuske, D., Satisfiability and model checking for MSO-definable temporal logics are in PSPACE, (CONCUR’03. CONCUR’03, Lect. Notes Comput. Sci., vol. 2761 (2003), Springer), 222-236 · Zbl 1195.68068 |
| [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 |
| [21] | Göller, S.; Lohrey, M.; Lutz, C., PDL with intersection and converse: satisfiability and infinite-state model checking, J. Symb. Log., 74, 1, 279-314 (2009) · Zbl 1181.03034 |
| [22] | Kamp, H., Tense logic and the theory of linear order (1968), University of California: University of California Los Angeles, Ph.D. thesis |
| [23] | La Torre, S.; Napoli, M., Reachability of multistack pushdown systems with scope-bounded matching relations, (CONCUR’11. CONCUR’11, Lect. Notes Comput. Sci., vol. 6901 (2011), Springer), 203-218 · Zbl 1343.68172 |
| [24] | La Torre, S.; Madhusudan, P.; Parlato, G., A robust class of context-sensitive languages, (LICS’07 (2007), IEEE Computer Society Press), 161-170 |
| [25] | La Torre, S.; Madhusudan, P.; Parlato, G., Context-bounded analysis of concurrent queue systems, (TACAS’08. TACAS’08, Lect. Notes Comput. Sci., vol. 4963 (2008), Springer), 299-314 · Zbl 1134.68446 |
| [26] | Lange, M.; Lutz, C., 2-ExpTime lower bounds for propositional dynamic logics with intersection, J. Symb. Log., 70, 5, 1072-1086 (2005) · Zbl 1100.03017 |
| [27] | Libkin, L., Logics for unranked trees: an overview, Log. Methods Comput. Sci., 2, 3:2, 1-31 (2006) · Zbl 1126.03039 |
| [28] | Madhusudan, P.; Parlato, G., The tree width of auxiliary storage, (POPL’11 (2011), ACM), 283-294 · Zbl 1284.68358 |
| [29] | Mennicke, R., Propositional dynamic logic with converse and repeat for message-passing systems, Log. Methods Comput. Sci., 9, 2:12, 1-35 (2013) · Zbl 1297.68171 |
| [30] | Musuvathi, M.; Qadeer, S., Iterative context bounding for systematic testing of multithreaded programs, (PLDI’07 (2007), ACM), 446-455 |
| [31] | Papadimitriou, C. H., Computational Complexity (1994), Addison-Wesley · Zbl 0833.68049 |
| [32] | Pnueli, A., The temporal logic of programs, (FOCS’77 (1977), IEEE), 46-57 |
| [33] | Qadeer, S.; Rehof, J., Context-bounded model checking of concurrent software, (TACAS’05. TACAS’05, Lect. Notes Comput. Sci., vol. 3440 (2005), Springer), 93-107 · Zbl 1087.68598 |
| [34] | Vardi, M. Y., The taming of converse: reasoning about two-way computations, (Proc. of the Conference on Logic of Programs (1985), Springer), 413-423 · Zbl 0603.68031 |
| [35] | Vardi, M. Y., Reasoning about the past with two-way automata, (ICALP’98. ICALP’98, Lect. Notes Comput. Sci. (1998), Springer), 628-641 · Zbl 0909.03019 |
| [36] | Zielonka, W., Notes on finite asynchronous automata, RAIRO Inform. Théor. Appl., 21, 99-135 (1987) · Zbl 0623.68055 |
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.
