Since the 80s, model checking (MC) has been applied to the automatic verification of hardware/software systems. Point-based temporal logics, such as LTL, CTL, CTL⁎, and the like, are commonly used in MC as the specification language; however, there are some inherently interval-based properties of computations, e.g., temporal aggregations and durations, that cannot be properly dealt with by these logics, as they model a state-by-state evolution of systems. Recently, an MC framework for the verification of interval-based properties of computations, based on Halpern and Shoham's interval temporal logic (HS, for short) and its fragments, has been proposed and systematically investigated. In this paper, we focus on the boundaries that separate tractable and intractable HS fragments in MC. We first prove that MC for the logic BE of Allen's relations started-by and finished-by is provably intractable, being EXPSPACE-hard. Such a lower bound immediately propagates to full HS. Then, in contrast, we show that other noteworthy HS fragments, i.e., the logic AA‾BB‾ (resp., AA‾EE‾) of Allen's relations meets, met-by, starts (resp., finishes), and started-by (resp., finished-by), are well-behaved, and turn out to have the same complexity as LTL (PSPACE-complete). Halfway are the fragments AA‾BB‾E‾ and AA‾EB‾E‾, whose EXPSPACE membership and PSPACE hardness are already known. Here, we give an original proof of EXPSPACE membership, that substantially simplifies the complexity of the constructions previously used for such a result. Contraction techniques—suitably tailored to each HS fragment—are at the heart of our results, enabling us to prove a pair of remarkable small-model properties

Which fragments of the interval temporal logic HS are tractable in model checking? / Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - 764:(2019), pp. 125-144. [10.1016/j.tcs.2018.04.011]

Which fragments of the interval temporal logic HS are tractable in model checking?

Bozzelli, Laura
;
Montanari, Angelo
;
Peron, Adriano
;
2019

Abstract

Since the 80s, model checking (MC) has been applied to the automatic verification of hardware/software systems. Point-based temporal logics, such as LTL, CTL, CTL⁎, and the like, are commonly used in MC as the specification language; however, there are some inherently interval-based properties of computations, e.g., temporal aggregations and durations, that cannot be properly dealt with by these logics, as they model a state-by-state evolution of systems. Recently, an MC framework for the verification of interval-based properties of computations, based on Halpern and Shoham's interval temporal logic (HS, for short) and its fragments, has been proposed and systematically investigated. In this paper, we focus on the boundaries that separate tractable and intractable HS fragments in MC. We first prove that MC for the logic BE of Allen's relations started-by and finished-by is provably intractable, being EXPSPACE-hard. Such a lower bound immediately propagates to full HS. Then, in contrast, we show that other noteworthy HS fragments, i.e., the logic AA‾BB‾ (resp., AA‾EE‾) of Allen's relations meets, met-by, starts (resp., finishes), and started-by (resp., finished-by), are well-behaved, and turn out to have the same complexity as LTL (PSPACE-complete). Halfway are the fragments AA‾BB‾E‾ and AA‾EB‾E‾, whose EXPSPACE membership and PSPACE hardness are already known. Here, we give an original proof of EXPSPACE membership, that substantially simplifies the complexity of the constructions previously used for such a result. Contraction techniques—suitably tailored to each HS fragment—are at the heart of our results, enabling us to prove a pair of remarkable small-model properties
2019
Which fragments of the interval temporal logic HS are tractable in model checking? / Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - 764:(2019), pp. 125-144. [10.1016/j.tcs.2018.04.011]
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0304397518302330-main.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Documento in Pre-print
Licenza: Accesso privato/ristretto
Dimensione 1.41 MB
Formato Adobe PDF
1.41 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/727614
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 1
social impact