Checking Interval Properties of Computations

TL;DR

This paper formalizes model checking for interval properties of computations using Halpern and Shoham's interval temporal logic, proving decidability and analyzing complexity over finite Kripke structures.

Contribution

It introduces an interpretation of HS logic over finite Kripke structures and establishes the decidability of model checking for interval properties.

Findings

Model checking for HS logic over finite Kripke structures is decidable.

A small model theorem is provided to support decidability.

The computational complexity of the problem is characterized with a lower bound.

Abstract

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g., a Kripke structure, and a formula specifying its expected behaviour, one can verify whether the system meets the behaviour by checking the formula against the model. Classically, system behaviour is expressed by a formula of a temporal logic, such as LTL and the like. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those constraining the temporal relations between pairs of temporally extended events or involving temporal aggregations, which are inherently "interval-based", and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over finite Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against finite Kripke structures is decidable by a suitable small model theorem, and we provide a lower bound to its computational complexity.