Since the late 80s, LTL and CTL model checking have been extensively applied in various areas of computer science and AI. Even though they proved themselves to be quite successful in many application domains, there are some relevant temporal conditions which are inherently “interval based” (this is the case, for instance, with telic statements like “the astronaut must walk home in an hour” and temporal aggregations like “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 order to 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 AABBE (resp., AAEBE) of Allen's interval relations meets, met-by, started-by (resp., finished-by), starts, and finishes. The proof exploits 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.
for reasoning about time [
In this paper, we make use of ITLs as the specification language in model
checking (MC), one of the most successful techniques in the area of formal
methods, which allows a user to automatically check whether some desired properties
of a system, specified by a temporal logic formula, hold over a model of it (usually
a Kripke structure). In order to verify interval properties of computations, one
needs to collect information about states into computation stretches: each finite
path in a Kripke structure is interpreted as an interval, whose labelling is defined
on the basis of the labelling of the component states. We focus our attention on
Halpern and Shoham’s modal logic of time intervals (HS) [
The MC problem for HS has been considered only very recently [
the current one, or are prefixes (resp., suffixes) or right/left-extensions of it. In [
to EXPSPACE is rather involved, and two very technical notions, namely, the
notions of scan function and configuration, are introduced in order to determine
the aforementioned bound to the length of representatives. Here, we provide a
much easier proof, which leads to another class of track representatives, with the
same purpose of those of [
Example
y v z z v v z z z z
fundamental elements of the MC problem for HS, and we give a short account of the known complexity results about MC for HS fragments. In Sect. 3, we introduce the notion of bisimilarity among tracks, that is exploited in Sect. 4, along with prefix samplings, to build, given a (generic) track ρ, a track ρ0 of bounded length, and indistinguishable from ρ with respect to satisfiability of
2
and their relative order was proposed by Allen in [
one modality for each Allen relation, but equality [
The language of HS consists of a set of proposition letters AP , the Boolean connectives ¬ and ∧, and a temporal modality for each of the (non trivial) Allen’s relations, i.e., hAi, hLi, hBi, hEi, hDi, hOi, hAi, hLi, hBi, hEi, hDi, and hOi. HS formulas are defined by the grammar ψ ::= p | ¬ψ | ψ ∧ ψ | hXiψ | hXiψ, where p ∈ AP and X ∈ {A, L, B, E, D, O}. In the following, we will also exploit the other usual logical connectives (disjunction ∨, implication →, and double implication ↔) as abbreviations. Furthermore, for any modality X, the dual universal modalities [X]ψ and [X]ψ are defined as ¬hXi¬ψ and ¬hXi¬ψ, respectively.
The joint nesting depth of B and E in a formula ψ, denoted by dBE(ψ), is defined as: (i) dBE(p) = 0, for any p ∈ AP ; (ii) dBE(¬ψ) = dBE(ψ); (iii) dBE(ψ ∧φ) = max{dBE(ψ), dBE(φ)}; (iv) dBE(hXi ψ) = 1+dBE(ψ), when X = B or X = E; (v) dBE(hXi ψ) = dBE(ψ), when both X 6= B and X 6= E. If we consider formulas ψ of HS fragments devoid of E (resp., B), the nesting depth of modality B (resp., E) in ψ, denoted as dB(ψ) (resp., dE(ψ)), accounts for modality B (resp., E) only, and dB(ψ) = dBE(ψ) (resp., dE(ψ) = dBE(ψ)).
HS fragment featuring existential (and universal) modalities for X1, .., Xn only.
W.l.o.g., we assume the non-strict semantics of HS, which admits intervals
consisting of a single point5. Under such an assumption, all HS modalities can
be expressed in terms of modalities hBi, hEi, hBi, and hEi [
Given an abstract interval model A = (AP , I, AI, BI, EI, σ) and an interval
– A, I |= p iff p ∈ σ(I), for any p ∈ AP ;
– A, I |= ¬ψ iff it is not true that A, I |= ψ (also denoted as A, I 6|= ψ);
– A, I |= ψ ∧ φ iff A, I |= ψ and A, I |= φ;
– A, I |= hXiψ, for X ∈ {A, B, E}, iff there is J ∈ I s.t. I XI J and A, J |= ψ;
– A, I |= hXiψ, for X ∈ {A, B, E}, iff there is J ∈ I s.t. J XI I and A, J |= ψ.
Kripke structures and abstract interval models. In the context of MC, finite state
systems are usually modelled as finite Kripke structures. In [
is the transition relation that describes the evolution of the system over time.
Fig. 1 depicts the finite Kripke structure vp0 vq1 {K(av0=,v0(){,p(,vq0},,v{1v)0, ,(vv11},v,δ0,),μ(,vv10,)v,1w)}h,eμre(v0δ) == {p}, and μ(v1) = { } q . The initial state v0 is
Fig. 1. The Kripke structure Ka. identified by a double circle.
Definition 3. A track ρ of a finite Kripke structure K = (AP , W, δ, μ, w0) is a finite sequence of states v1 · · · vn, with n ≥ 1, s.t. (vi, vi+1) ∈ δ for i ∈ [1, n − 1]. 5 All the results we prove in the paper hold for the strict semantics as well. Let TrkK be the (infinite) set of all tracks over a finite Kripke structure K . For any track ρ = v1 · · · vn ∈ TrkK , we define: – |ρ| = n, fst(ρ) = v1, and lst(ρ) = vn; – any index i ∈ [1, |ρ|] is called a ρ-position and ρ(i) = vi; – states(ρ) = {v1, · · · , vn} ⊆ W ; – ρ(i, j) = vi · · · vj , for 1 ≤ i ≤ j ≤ |ρ|, is the subtrack of ρ bounded by i, j; – Pref(ρ) = {ρ(1, i) | 1 ≤ i ≤ |ρ| − 1} and Suff(ρ) = {ρ(i, |ρ|) | 2 ≤ i ≤ |ρ|} are the sets of all proper prefixes and suffixes of ρ, respectively.
Moreover, if lst(ρ) = fst(ρ0), we denote by ρ ? ρ0 the track ρ(1, |ρ| − 1) · ρ0. In particular, when |ρ| = 1, ρ ? ρ0 = ρ0. In the following, when we write ρ ? ρ0, we implicitly assume that lst(ρ) = fst(ρ0). Finally, if fst(ρ) = w0 (the initial state of K ), ρ is called an initial track.
An abstract interval model (over TrkK ) can be naturally associated with a finite Kripke structure K by considering the set of intervals as the set of tracks of K . Since K has loops (δ is left-total), the number of tracks in TrkK , and thus the number of intervals, is infinite.
ture K = (AP , W, δ, μ, w0) is AK = (AP , I, AI, BI, EI, σ), where I = TrkK , AI = {(ρ, ρ0) ∈ I × I | lst(ρ) = fst(ρ0)}, BI = {(ρ, ρ0) ∈ I × I | ρ0 ∈ Pref(ρ)}, EI = {(ρ, ρ0) ∈ I × I | ρ0 ∈ Suff(ρ)}, and σ : I 7→ 2AP is such that σ(ρ) = Tw∈states(ρ) μ(w), for all ρ ∈ I.
Relations AI, BI, and EI are interpreted as the Allen’s relations A, B, and
ρ = v1 · · · vn if and only if it holds over all the states v1, · · · , vn of ρ. This conforms
to the homogeneity principle [
Definition 5. Let K be a finite Kripke structure and ψ be an HS formula; we say that a track ρ ∈ TrkK satisfies ψ, denoted as K , ρ |= ψ, iff it holds that AK , ρ |= ψ. Moreover, we say that K models ψ, denoted as K |= ψ, iff for all initial tracks ρ0 ∈ TrkK it holds that K , ρ0 |= ψ. The model checking problem for HS over finite Kripke structures is the problem of deciding whether K |= ψ.
In Fig. 2, we provide an example of a finite Kripke structure KSched that
models the behaviour of a scheduler serving three processes which are continuously
requesting the use of a common resource (it is a simplified version of an example
given in [
u1
ful properties to be checked against KSched can be expressed in HS, in particular, by formulas of AAEBE. In all formulas, we force the validity of the considered property over all legal computation sub-intervals by using modality [E] (all computation sub-intervals are suffixes of at least one initial track). The truth of the next statements can easily be checked (hEik stands for k occurrences of modality hEi):
E 3 – KSched |= [E] h i > → (χ(p1, p2) ∨ χ(p1, p3) ∨ χ(p2, p3)) , – wKShcehreed χ6|=(p[,Eq)](:h=Eih1E0i hAi p ∧ hEi hAi q;
> → hEi hAi p3); – KSched 6|= [E](hEi5 → (hEi hAi p1 ∧ hEi hAi p2 ∧ hEi hAi p3)).
The first formula states that in any suffix of length at least 4 of an initial track, at least 2 proposition letters are witnessed. KSched satisfies the formula since a process cannot be executed twice in a row. The second formula states that in any suffix of length at least 11 of an initial track, process 3 is executed at least once in some internal states (non starvation). KSched does not satisfy the formula since the scheduler can avoid executing a process ad libitum. The third formula states that in any suffix of length at least 6 of an initial track, p1, p2, p3 are all witnessed. The only way to satisfy this property is to constrain the scheduler to execute the 3 processes in a strictly periodic manner, but this is not the case.
In [
succinct AABBE
EXPSPACE 2
NEXP-hard 2 AABBE
EXPSPACE 2 PSPACE-hard 3 full HS nonELEMENTARY 1
EXPSPACE-hard 5
hardness BE nonELEMENTARY 1
EXPSPACE-hard 5 hardness
AABB PSPACE-complete 5
AAEE PSPACE-complete 5 AABE PSPACE-complete 2,3
AA
PNP[O(log2 n)] 4
PNP[O(log n)]-hard 4 E coNP-complete 5 B coNP-complete 5
hardness hardness upper-bound
hardness hardness hardness
hardness E PSPACE-complete 4 B PSPACE-complete 4 A
PNP[O(log2 n)] 4 PNP[O(log n)]-hard 4
Prop coNP-complete 3
AABBE and AAEBE is PSPACE-hard (with a succinct encoding of formulas the
algorithm remains in EXPSPACE, but a NEXPTIME lower bound can be
given [
(compared to [
bisimilarity between a pair of tracks ρ and ρ0 of a Kripke structure. As proved by Proposition 2 below, prefix-bisimilarity (resp., suffix-bisimilarity) is a sufficient condition for two tracks ρ and ρ0 to be indistinguishable with respect to satisfiability of (some classes of) AABBE (resp., AAEBE) formulas, respectively. Definition 6 (Prefix-bisimilarity and Suffix-bisimilarity). Let h ≥ 0 and ρ and ρ0 be two tracks of a Kripke structure K . We say that ρ and ρ0 are h-prefix bisimilar if the following conditions inductively hold: – for h = 0: fst(ρ) = fst(ρ0), lst(ρ) = lst(ρ0), and states(ρ) = states(ρ0). – for h > 0: ρ and ρ0 are 0-prefix bisimilar and for each proper prefix ν of ρ (resp., proper prefix ν0 of ρ0), there exists a proper prefix ν0 of ρ0 (resp., proper prefix ν of ρ) such that ν and ν0 are (h − 1)-prefix bisimilar.
The notion of h-suffix bisimilarity is defined in a symmetric way by considering suffixes of tracks instead of prefixes.
bisimilarity is an equivalence relation over TrkK .
Moreover, h-suffix bisimilarity and h-prefix bisimilarity propagate downwards.
Proposition 1. Let h ≥ 0, and ρ and ρ0 be two h-prefix (resp., h-suffix) bisimilar tracks of a Kripke structure K . Then, for each track ρ00 of K , 1. ρ00 ? ρ and ρ00 ? ρ0 are h-prefix (resp., h-suffix) bisimilar; 2. ρ ? ρ00 and ρ0 ? ρ00 are h-prefix (resp., h-suffix) bisimilar.
of formulas, we obtain that h-prefix (resp., h-suffix) bisimilarity preserves the satisfiability of AABBE (resp., AAEBE) formulas having nesting depth of modality B (resp., E) at most h.
Proposition 2. Let h ≥ 0, and ρ and ρ0 be two h-prefix (resp., h-suffix) bisimilar tracks of a Kripke structure K . For each AABBE (resp., AAEBE) formula ψ with dB(ψ) ≤ h (resp., dE(ψ) ≤ h), it holds that K , ρ |= ψ iff K , ρ0 |= ψ. 4
symmetric). We shall show how to determine a subset of positions of a track ρ (a prefix sampling of ρ), starting from which it is possible to build another track ρ0, of bounded exponential size, which is indistinguishable from ρ with respect to the fulfilment of AABBE formulas up to a given nesting depth of modality B (exponential-size model-track property). We start by introducing the notions of induced track, prefix-skeleton sampling, and h-prefix sampling, and prove some related properties.
Definition 7 (Induced track). Let ρ be a track of length n of a Kripke structure K . A track induced by ρ is a track π of K such that there exists an increasing sequence of ρ-positions i1 < . . . < ik, with i1 = 1, ik = n, and π = ρ(i1) · · · ρ(ik). Note that if π is induced by ρ, then fst(π) = fst(ρ), lst(π) = lst(ρ), and |π| ≤ |ρ| (in particular, |π| = |ρ| iff π = ρ). Intuitively, a track induced by ρ is obtained by contracting ρ, namely, by concatenating some subtracks of ρ, provided that the resulting sequence is a track of K as well.
In the following, given a set I of natural numbers, by “two consecutive elements of I” we refer to a pair of elements i, j ∈ I s.t. i < j and I ∩ [i, j] = {i, j}. Definition 8 (Prefix-skeleton sampling). Let ρ be a track of a Kripke structure K = (AP , W, δ, μ, w0). Given two ρ-positions i and j, with i ≤ j, the prefixskeleton sampling of ρ(i, j) is the minimal set P of ρ-positions in the interval [i, j] satisfying: (i) i, j ∈ P ; (ii) for each state w ∈ W occurring along ρ(i + 1, j − 1), the minimal position k ∈ [i + 1, j − 1] such that ρ(k) = w is in P .
P of (any) track ρ(i, j) is such that |P | ≤ |W | + 2 and i + 1 ∈ P whenever i < j. Definition 9 (h-prefix sampling). Let ρ be a track of a Kripke structure K . For each h ≥ 1, the h-prefix sampling of ρ is the minimal set Ph of ρ-positions inductively satisfying the following conditions: – Base case: h = 1. P1 is the prefix-skeleton sampling of ρ; – Inductive step: h > 1. (i) Ph ⊇ Ph−1 and (ii) for all pairs of consecutive positions i, j in Ph−1, the prefix-skeleton sampling of ρ(i, j) is in Ph.
sampling Ph of ρ is such that |Ph| ≤ (|W | + 2)h.
Lemma 1. Let h ≥ 1, ρ be a track of K , and i, j be two consecutive ρ-positions in the h-prefix sampling of ρ. Then, for all ρ-positions n, n0 ∈ [i + 1, j] such that ρ(n) = ρ(n0), it holds that ρ(1, n) and ρ(1, n0) are (h − 1)-prefix bisimilar.
– Base case: h = 1. The 1-prefix sampling of ρ is the prefix-skeleton sampling of ρ. Hence, being i and j consecutive positions in this sampling, for each position k ∈ [i, j − 1], there is ` ≤ i such that ρ(`) = ρ(k). Since ρ(n) = ρ(n0), states(ρ(1, n)) = states(ρ(1, n0)), so ρ(1, n) and ρ(1, n0) are 0-prefix bisimilar. – Inductive step: h > 1. By definition of h-prefix sampling, there are two consecutive positions i0, j0 in the (h − 1)-prefix sampling of ρ such that i, j are consecutive positions of the prefix-skeleton sampling of ρ(i0, j0). If i = i0, then j = i + 1, hence, being n, n0 ∈ [i + 1, j], we get that n = n0, and the result trivially holds.
Now, assume that i 6= i0, thus i > i0. As in the base case, we easily deduce that ρ(1, n) and ρ(1, n0) are 0-prefix bisimilar. It remains to show that for each proper prefix ν of ρ(1, n) (resp., proper prefix ν0 of ρ(1, n0)), there is a proper prefix ν0 of ρ(1, n0) (resp., proper prefix ν of ρ(1, n)) such that ν and ν0 are (h − 2)-prefix bisimilar. Let us consider a proper prefix ν of ρ(1, n) (the proof for the other direction is symmetric). Hence, ν = ρ(1, m) for some m < n. We distinguish two cases: • m ≤ i. Hence ρ(1, m) is a proper prefix of ρ(1, n0) and the result follows. • m > i: since i and j are consecutive positions of the prefix-skeleton sampling of ρ(i0, j0), i > i0, and m ∈ [i + 1, j − 1] (hence m < j0), there exists m0 ∈ [i0 + 1, i] such that ρ(m0) = ρ(m) and m0 is in the prefix-skeleton sampling of ρ(i0, j0). Let ν0 = ρ(1, m0). Evidently ν0 is a proper prefix of ρ(1, n0) (as n0 ≥ i + 1). Moreover, since m, m0 ∈ [i0 + 1, j0] and i0, j0 are consecutive positions in the (h − 1)-prefix sampling of ρ, by the inductive hypothesis ν = ρ(1, m) and ν0 = ρ(1, m0) are (h − 2)-prefix bisimilar. tu
ρ of a Kripke structure, another track ρ0, induced by ρ and h-prefix bisimilar to ρ, such that |ρ0| ≤ (|W | + 2)h+2. By Proposition 2, ρ0 is indistinguishable from ρ w.r.t. the fulfilment of any AABBE formula ψ with dB(ψ) ≤ h.
In order to build ρ0, we first compute the (h + 1)-prefix sampling Ph+1 of ρ.
induced by ρ(i, j), with no repeated occurrences of any state, except at most the first and last ones (hence, it is no longer than (|W | + 2)). The track ρ0 is just the ordered concatenation (by means of the ? operator) of all these tracks. The aforementioned bound on |ρ0| holds as, by Property 3, |Ph+1| ≤ (|W |+2)h+1. The following preparatory lemma states that ρ and ρ0 are indeed h-prefix bisimilar. Lemma 2. Let h ≥ 1, ρ be a track of K , and ρ0 = ρ(i1)ρ(i2) · · · ρ(ik) be a track induced by ρ, where 1 = i1 < i2 < . . . < ik = |ρ| and Ph+1 ⊆ {i1, . . . , ik}, with Ph+1 the (h + 1)-prefix sampling of ρ. Then, for all j ∈ [1, k], ρ0(1, j) and ρ(1, ij ) are h-prefix bisimilar.
Notice that, in particular, ρ and ρ0 are h-prefix bisimilar.
Proof. Let Q = {i1, . . . , ik} (hence Ph+1 ⊆ Q) and let j ∈ [1, k]. We prove by induction on j that ρ0(1, j) and ρ(1, ij ) are h-prefix bisimilar. As for the base case (j = 1), the result holds, since i1 = 1.
Now assume that j > 1. We first show that ρ(1, ij ) and ρ0(1, j) are 0-prefix bisimilar. Clearly, ρ(1) = ρ(i1) = ρ0(1), ρ(ij ) = ρ0(j), and states(ρ0(1, j)) ⊆ states(ρ(1, ij )). Now, if, by contradiction, there was a state w such that w ∈ states(ρ(1, ij )) \ states(ρ0(1, j)), then for all l ∈ Q, with l ≤ ij , ρ(l) 6= w. However, the prefix-skeleton sampling P1 of ρ is contained in Q, and the minimal ρ-position l0 such that ρ(l0) = w belongs to P1. Since w ∈ states(ρ(1, ij )), l0 ≤ ij . Thus, we get a contradiction, implying that states(ρ0(1, j)) = states(ρ(1, ij )).
It remains to prove that: (1) for each proper prefix ν0 of ρ0(1, j), there exists a proper prefix ν of ρ(1, ij ) such that ν and ν0 are (h − 1)-prefix bisimilar, and (2) for each proper prefix ν of ρ(1, ij ), there exists a proper prefix ν0 of ρ0(1, j) such that ν and ν0 are (h − 1)-prefix bisimilar.
such that ν0 = ρ0(1, m). By the inductive hypothesis, ρ0(1, m) and ρ(1, im) are h-prefix bisimilar, and thus (h − 1)-prefix bisimilar as well (Property 2). Since ρ(1, im) is a proper prefix of ρ(1, ij ), by choosing ν0 = ρ(1, im) (1) follows.
As for (2), assume that ν is a proper prefix of ρ(1, ij ). Therefore, there exists n ∈ [1, ij − 1] such that ν = ρ(1, n). We distinguish two cases: – n ∈ Ph+1. Since n < ij , there exists m ∈ [1, j − 1] such that n = im. By the inductive hypothesis, ρ(1, n) and ρ0(1, m) are h-prefix bisimilar, and thus (h − 1)-prefix bisimilar as well (Property 2). Since ρ0(1, m) is a proper prefix of ρ0(1, j), by choosing ν0 = ρ0(1, m) (2) follows. – n ∈/ Ph+1. It follows that there exist two consecutive positions i0 and j0 in Ph+1, with i0 < j0, such that n ∈ [i0 + 1, j0 − 1]. By definition of (h + 1)-prefix sampling, there exist two consecutive positions i00 and j00 in the h-prefix sampling of ρ, with i00 < j00, such that i0 and j0 are two consecutive positions in the prefix-skeleton sampling of ρ(i00, j00).
First, we observe that i0 6= i00 (otherwise, j0 = i0 + 1, which contradicts the fact that [i0 + 1, j0 − 1] 6= ∅, as n ∈ [i0 + 1, j0 − 1]). Thus, by definition of prefix-skeleton sampling applied to ρ(i00, j00), and since n ∈ [i0 + 1, j0 − 1], there must be ` ∈ [i00 + 1, i0] such that ρ(`) = ρ(n) and ` is in the prefixskeleton sampling of ρ(i00, j00). Hence ` ∈ Ph+1 by definition of (h + 1)-prefix sampling. As a consequence, since ` < n < ij , there exists m ∈ [1, j − 1] such that ` = im. By applying Lemma 1, we deduce that ρ(1, n) and ρ(1, im) are (h − 1)-prefix bisimilar. Moreover, by the inductive hypothesis, ρ(1, im) and ρ0(1, m) are (h − 1)-prefix bisimilar. Thus, by choosing ν0 = ρ0(1, m), ν0 is a proper prefix of ρ0(1, j) which is (h − 1)-prefix bisimilar to ν = ρ(1, n). tu Theorem 1 (Exponential-size model-track property for AABBE). Let ρ be a track of a Kripke structure K and h ≥ 0. Then, there exists a track ρ0 induced by ρ, whose length is at most (|W | + 2)h+2, such that for every AABBE formula ψ with dB(ψ) ≤ h, it holds that K , ρ |= ψ iff K , ρ0 |= ψ.
Proof. Let Ph+1 be the (h + 1)-prefix sampling of ρ. For all pairs of consecutive ρ-positions i and j in Ph+1, there exists a track induced by ρ(i, j) having length at most |W | + 2, featuring no repeated occurrences of any internal state. We now define ρ0 as the track of K obtained by concatenating in order all these induced tracks by means of the ? operator. It is immediate to see that ρ0 = ρ(i1)ρ(i2) · · · ρ(ik), for some indexes 1 = i1 < i2 < · · · < ik = |ρ|, where {i1, . . . , ik} contains the (h + 1)-prefix sampling Ph+1 of ρ. It holds that |ρ0| ≤ |Ph+1| · (|W | + 2) and since, by Property 3, |Ph+1| ≤ (|W | + 2)h+1, we obtain that |ρ0| ≤ (|W | + 2)h+2. Moreover, by Lemma 2, ρ and ρ0 are h-prefix bisimilar. By Proposition 2, the result follows. tu
same as that presented in [
tracks of a Kripke structure to solve the MC problem for the HS fragments
representatives given for the same problem in [