×

Visibly linear dynamic logic. (English) Zbl 1400.68059

Summary: We introduce Visibly Linear Dynamic Logic (VLDL), which extends Linear Temporal Logic (LTL) by temporal operators that are guarded by visibly pushdown languages over finite words. In VLDL one can, e.g., express that a function resets a variable to its original value after its execution, even in the presence of an unbounded number of intermediate recursive calls. We prove that VLDL describes exactly the \(\omega\)-visibly pushdown languages, i.e., that it is strictly more expressive than LTL and able to express recursive properties of programs with unbounded call stacks.
The main technical contribution of this work is a translation of VLDL into \(\omega\)-visibly pushdown automata of exponential size via one-way alternating jumping automata. This translation yields exponential-time algorithms for satisfiability, validity, and model checking. We also show that visibly pushdown games with VLDL winning conditions are solvable in triply-exponential time. We prove all these problems to be complete for their respective complexity classes.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B44 Temporal logic
68Q25 Analysis of algorithms and problem complexity
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

MOPS
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

References:

[1] Weinert, A.; Zimmermann, M., Visibly linear dynamic logic, (Lal, A.; Akshay, S.; Saurabh, S.; Sen, S., FSTTCS 2016, LIPIcs, vol. 65, (2016), Schloss Dagstuhl - LZI), 28:1-28:14 · Zbl 1391.68022
[2] Pnueli, A., The temporal logic of programs, (FOCS 1977, (1977), IEEE), 46-57
[3] Leucker, M.; Sanchéz, C., Regular linear temporal logic, (Jones, C. B.; Liu, Z.; Woodcock, J., ICTAC 2007, LNCS, vol. 4711, (2007)) · Zbl 1147.03305
[4] Vardi, M., The rise and fall of LTL, (D’Agostino, G.; Torre, S. L., EPTCS 54, (2011))
[5] Vardi, M.; Wolper, P., Reasoning about infinite computations, Inform. and Comput., 115, 1-37, (1994) · Zbl 0827.03009
[6] Wolper, P., Temporal logic can be more expressive, Inf. Control, 56, 72-99, (1983) · Zbl 0534.03009
[7] Alur, R.; Madhusudan, P., Visibly pushdown languages, (STOC 2004, (2004), ACM), 202-211 · Zbl 1192.68396
[8] Alur, R.; Etessami, K.; Madhusudan, P., A temporal logic of nested calls and returns, (TACAS 2004, LNCS, vol. 2988, (2004), Springer), 467-481 · Zbl 1126.68466
[9] Bozzelli, L., Alternating automata and a temporal fixpoint calculus for visibly pushdown languages, (Caires, L.; Vasconcelos, V. T., CONCUR 2007, LNCS, vol. 4703, (2007), Springer), 476-491 · Zbl 1151.68458
[10] Löding, C.; Madhusudan, P.; Serre, O., Visibly pushdown games, (Lodaya, L.; Mahajan, M., FSTTCS 2004, LNCS, vol. 3328, (2005), Springer), 408-420 · Zbl 1117.68409
[11] Bouajjani, A.; Esparza, J.; Maler, O., Reachability analysis of pushdown automata: application to model-checking, (Mazurkiewicz, A.; Winkowski, J., CONCUR 1997, LNCS, vol. 1243, (1997), Springer), 135-150, full version available at
[12] Bozzelli, L.; Sánchez, C., Visibly linear temporal logic, (IJCAR 2014, LNCS, vol. 8562, (2014)), 418-483 · Zbl 1423.68274
[13] Weinert, A., VLDL satisfiability and model checking via tree automata, (Lokam, S.; Ramanujam, R., FSTTCS 2017, LIPIcs, vol. 93, (2017), Schloss Dagstuhl - LZI), 47:1-47:13
[14] Faymonville, P.; Zimmermann, M., Parametric linear dynamic logic, Inform. and Comput., 253, 237-256, (2017) · Zbl 1362.68169
[15] Thompson, K., Programming techniques: regular expression search algorithm, Commun. ACM, 11, 6, 419-422, (1968) · Zbl 0164.46205
[16] Chen, H.; Wagner, D., MOPS: an infrastructure for examining security properties of software, (Atluri, V., CCS 2002, (2002), ACM), 235-244
[17] Bozzelli, L.; Sánchez, C., Visibly rational expressions, Acta Inform., 51, 1, 25-49, (2014) · Zbl 1354.68148
[18] Chandra, A.; Stockmeyer, L., Alternation, (FOCS 1976, (1976), IEEE), 98-108
[19] Hopcroft, J.; Motwani, R.; Ullman, J., Introduction to automata theory, languages, and computation, (2001), Addison-Wesley · Zbl 0980.68066
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.