In this paper, we introduce and investigate an extension of Halpern and Shoham’s interval temporal logic HS for the specification and verification of branching-time context-free requirements of pushdown systems under a state-based semantics over Kripke structures. Both homogeneity and visibility are assumed. The proposed logic, called nested BHS, supports branching-time both in the past and in the future, and is able to express non-regular properties of linear and branching behaviours of procedural contexts in a natural way. It strictly subsumes well-known linear time context-free extensions of LTL such as CaRet [R. Alur et al., 2004] and NWTL [R. Alur et al., 2007]. The main result is the decidability of the visibly pushdown model-checking problem against nested BHS. The proof exploits a non-trivial automata-theoretic construction.
@InProceedings{bozzelli_et_al:LIPIcs.FSTTCS.2019.33, author = {Bozzelli, Laura and Montanari, Angelo and Peron, Adriano}, title = {{Interval Temporal Logic for Visibly Pushdown Systems}}, booktitle = {39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)}, pages = {33:1--33:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-131-3}, ISSN = {1868-8969}, year = {2019}, volume = {150}, editor = {Chattopadhyay, Arkadev and Gastin, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.33}, URN = {urn:nbn:de:0030-drops-115959}, doi = {10.4230/LIPIcs.FSTTCS.2019.33}, annote = {Keywords: Pushdown systems, Interval temporal logic, Model checking} }
Feedback for Dagstuhl Publishing