Model checking is one of the most successful techniques in system verification. While a variety of methods and tools exist to check properties expressed in point-based temporal logics, like LTL and CTL, model checking for interval temporal logic has entered the research agenda only very recently. In previous work, we devised a non-elementary model checking procedure for Halpern and Shoham's modal logic of time intervals, interpreted over finite Kripke structures, and an EXPSPACE algorithm for two meaningful fragments of it. In this paper, we show that the latter algorithm can be suitably tailored in order to check a subset of the computations of a system, that satisfy a given bound on the number of cycle alternations, by making use of a polynomial (instead of exponential) working space. We also prove that such a revised algorithm turns out to be complete for Kripke structures whose strongly connected components are simple cycles

Constraining Cycle Alternations in Model Checking for Interval Temporal Logic

MOLINARI, ALBERTO;MONTANARI, Angelo;
2016-01-01

Abstract

Model checking is one of the most successful techniques in system verification. While a variety of methods and tools exist to check properties expressed in point-based temporal logics, like LTL and CTL, model checking for interval temporal logic has entered the research agenda only very recently. In previous work, we devised a non-elementary model checking procedure for Halpern and Shoham's modal logic of time intervals, interpreted over finite Kripke structures, and an EXPSPACE algorithm for two meaningful fragments of it. In this paper, we show that the latter algorithm can be suitably tailored in order to check a subset of the computations of a system, that satisfy a given bound on the number of cycle alternations, by making use of a polynomial (instead of exponential) working space. We also prove that such a revised algorithm turns out to be complete for Kripke structures whose strongly connected components are simple cycles
File in questo prodotto:
File Dimensione Formato  
paper 18.pdf

Open Access dal 01/12/2017

Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 342.44 kB
Formato Adobe PDF
342.44 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/1089177
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact