License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2019.33
URN: urn:nbn:de:0030-drops-115959
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11595/
Go to the corresponding LIPIcs Volume Portal

Bozzelli, Laura ; Montanari, Angelo ; Peron, Adriano

Interval Temporal Logic for Visibly Pushdown Systems

pdf-format:
LIPIcs-FSTTCS-2019-33.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{bozzelli_et_al:LIPIcs:2019:11595,
  author =	{Laura Bozzelli and Angelo Montanari and Adriano Peron},
  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 =	{Arkadev Chattopadhyay and Paul Gastin},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2019/11595},
  URN =		{urn:nbn:de:0030-drops-115959},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.33},
  annote =	{Keywords: Pushdown systems, Interval temporal logic, Model checking}
}

Keywords: Pushdown systems, Interval temporal logic, Model checking
Collection: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)
Issue Date: 2019
Date of publication: 04.12.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI