Since the late 80s, LTL and CTL model checking have been extensively applied in various areas of computer science and AI. Even thoughtheyprovedthemselvestobe quitesuccessfulin manyapplication domains,therearesomerelevanttemporalconditionswhichareinherently “interval based” (this is the case, for instance, with telic statements like “theastronautmustwalkhomeinanhour”andtemporalaggregationslike “the average speed of the rover cannot exceed the established threshold”) and thus cannot be properly modelled by point-based temporal logics. In general, to check interval properties of the behavior of a system, one needs to collect information about states into behavior stretches, which amounts to interpreting each finite sequence of states as an interval and to suitably defining its labelling on the basis of the labelling of the states that compose it. In orderto deal with these properties,a model checking framework based on Halpern and Shoham’s interval temporal logic (HS for short) and its fragments has been recently proposed and systematically investigated in the literature. In this paper, we give an original proof of EXPSPACE membership of the model checking problem for the HS fragment AAbarBBbarE (resp.,AAbarEBEbar)ofAllen’sintervalrelationsmeets,met-by,started-by (resp., finished-by),starts,andfinishes. The proofexploits track bisimilarity and prefix sampling, and it turns out to be much simpler than the previously known one. In addition, it improves some upper bounds.

Interval temporal logic model checking based on track bisimilarity and prefix sampling

Bozzelli, Laura
;
Molinari, Alberto;Montanari, Angelo
;
Peron, Adriano
;
2016

Abstract

Since the late 80s, LTL and CTL model checking have been extensively applied in various areas of computer science and AI. Even thoughtheyprovedthemselvestobe quitesuccessfulin manyapplication domains,therearesomerelevanttemporalconditionswhichareinherently “interval based” (this is the case, for instance, with telic statements like “theastronautmustwalkhomeinanhour”andtemporalaggregationslike “the average speed of the rover cannot exceed the established threshold”) and thus cannot be properly modelled by point-based temporal logics. In general, to check interval properties of the behavior of a system, one needs to collect information about states into behavior stretches, which amounts to interpreting each finite sequence of states as an interval and to suitably defining its labelling on the basis of the labelling of the states that compose it. In orderto deal with these properties,a model checking framework based on Halpern and Shoham’s interval temporal logic (HS for short) and its fragments has been recently proposed and systematically investigated in the literature. In this paper, we give an original proof of EXPSPACE membership of the model checking problem for the HS fragment AAbarBBbarE (resp.,AAbarEBEbar)ofAllen’sintervalrelationsmeets,met-by,started-by (resp., finished-by),starts,andfinishes. The proofexploits track bisimilarity and prefix sampling, and it turns out to be much simpler than the previously known one. In addition, it improves some upper bounds.
File in questo prodotto:
File Dimensione Formato  
ITCTS2016.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Accesso privato/ristretto
Dimensione 519.92 kB
Formato Adobe PDF
519.92 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/11588/745106
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact