An Epistemic Halpern-Shoham Logic

1 Introduction

In the past ten years there has been considerable work aimed at verifying specifications of multi-agent systems (MAS) by means of model checking [Clarke et al., 1999]. Several techniques have been developed including binary decision diagrams [Raimondi and Lomuscio, 2005; Gammie and van der Meyden, 2004], symmetry reduction [Cohen et al., 2009] and bounded model checking [Lomuscio et al., 2007]. While in reactive systems plain temporal logic is normally used, several agent-based logical languages have been employed to specify MAS. These include BDI logic [Rao, 1996], ATL [Alur et al., 1996], and temporal-epistemic logic [Fagin et al., 1995]. The latter has received considerable attention due to a number of agent-based applications that benefit from a knowledge-based approach.

Model checking approaches for temporal-epistemic specifications have covered different assumptions on the flow of time. Linear Temporal Logic (LTL) was assumed in some lines [van der Hoek and Wooldridge, 2003], Computational Tree Logic (CTL) was employed in others [Raimondi and Lomuscio, 2005]. These variants share a single underlying principle: formulas are evaluated at a state. However, there is a long and successful tradition in temporal reasoning that explores the implications of interpreting formulas on intervals, not at states. Two most popular approaches are the Halpern-Shoham Logic [Halpern and Shoham, 1991] and Interval Temporal Logic [Moszkowski, 1983].

Reasoning about intervals is useful when one needs to express naturally properties that hold continuously between two instances of time. For example, in the interval-based HalpernShoham logic (HS) one can naturally state whether in a given interval I, every occurrence of "request" (a propositional variable that labels point intervals) during the interval is followed by an occurrence of "fulfil", represented by the formula [E](〈B〉request ⇒ 〈D〉fulfil ∨ 〈E〉fulfil). HS logic includes twelve modal operators expressing various conditions expressing temporal order between intervals, e.g., "begins", "overlaps", etc. Since the seminal work in the area showed that the satisfiability problem for HS logic is undecidable [Halpern and Shoham, 1991], much of the recent literature has focused on the identification of decidable fragments of HS logic and the assessment of their computational complexity. There are 212 different sub-logics of HS logic; the complexity of their satisfiability problem is now known for the great majority of them [Monica et al., 2011].

Against this background, our long term goals is to develop and use interval-based specifications for reasoning about MAS. We have two objectives for this paper. Firstly, as we are interested in providing powerful languages for the specification of MAS, we put forward a family of epistemic logics based on HS. Secondly, since we are ultimately interested in their use in practice, we define and study their model checking problem. Our results show that natural, knowledgebased concepts can be defined on intervals and that there are fragments of epistemic variants of fragments of HS with a PSPACE-complete model checking problem. Our experience shows that most real-life specifications do not use a deep nesting of knowledge operators. As we show, fragments with bounded knowledge depth are even easier as they are NPcomplete, or even in PTIME.

The rest of the paper is organised as follows. In Section 2 we define interval-based interpreted systems, the semantics we introduce for reasoning about intervals and knowledge in a MAS, and define their model checking problem. In Section 3 we introduce an epistemic logic, whose satisfaction is defined on intervals and explore its model checking problem. We extend these investigations in Section 4 by adding a restricted number of interval operators and combine them with epistemic modalities. Section 5 is dedicated to some noteworthy special cases with very attractive computational complexity. We conclude in Section 6, where we also discuss related work.

2 Interval-Based Interpreted Systems

In this section we introduce interval-based interpreted systems, a novel semantics to interpret a variety of temporal and epistemic logics on temporal intervals, and give a general definition of the model checking problem on them.

To begin, we say that an order (S,≤) is tree-like if it is a transitive closure of a tree, i.e., it satisfies the following properties:

• The order is strongly discrete, i.e., the are only finitely many points between any two points.
• The order contains the least element.
• For any a, b, c ∈ S, if a ≤ c and b ≤ c, then either a ≤ b or b ≤ a.

In line with the literature on interpreted systems [Fagin et al., 1995] in the following we assume a finite set of agents A = {1, . . . ,m}. Each agent is endowed with a set of local states Li, i ∈ A. We also consider an environment e and its corresponding set of local states Le. As standard in interpreted systems we assume each agent is equipped with a set of local actions and a local protocol function, which, as usual, through joint-actions, produces a transition relation t. We define systems purely on the basis of the transition relation.

Definition 1. An interval-based interpreted system, or IBIS, is a tuple IS = (S, s0, t, L), where:

• The set S ⊆ Le×L1×· · ·×Lm is a set of global states, reachable from s0 via t;
• The state s0 ∈ S is the initial global state of the system;
• t ⊆ S2 is a transition relation such that 〈S, t〉 is a treelike order and s0 is its least element,
• L : S2 → 2Var is a labelling function, where Var is a set of propositional variables.

Given an IBIS IS, an interval in IS is a finite path on IS, i.e., a sequence of states I = s1s2 . . . sn such that sitsi+1, 1 ≤ i ≤ (n - 1). A point interval is an interval that consists of exactly one state.

In general interval-based interpreted systems are infinite. To define the model checking problem, we introduce a compact representation of IBIS, called generalised Kripke structures (GSK).

We consider the assumptions of Definition 1.

Definition 2. A generalised Kripke structure, or a model, is a tuple M = (S, s0, t, L), where:

• The set S ⊆ Le ×L1 × · · · ×Lm is the set of reachable global states,
• s0 ∈ S is an initial global state,
• t ⊆ S2 is the transition relation,
• L : S2 → 2Var is a labelling function for a set of atoms Var .

We extend the definition of L to intervals by considering L([a, b]) = L(a, b). For a global state s = (le, l1, . . . , lm), we denote by li(s) the local state li ∈ Li of agent i ∈ A in s. Note that, differently from standard temporal-epistemic logic, the structures above admit the labelling of propositions at pairs of states and not at a single state.

To see that GKS are compact representations of IBIS, we define their unravelling as follows.

Definition 3. Given a GKS M = (S, s0, t, L), its unravelling IS = ( ˆ S, so, ˆ t, ˆL) is defined as follows:

• ¯ S = ⋃∞i=0 ¯ Si is the set of all finite paths in M starting from s0, i.e., all ¯ Si are defined by the induction rules: ¯ S0 = {s0};

¯ Si = {s0 . . . si+1 | s0 . . . si-1 ∈ ¯ Si-1 ∧(si-1, si) ∈ t}, for i > 0.

• ˆ t is the transitive closure of the relation ¯ t defined by: s¯ ts′ iff dpt(s′ ) = dpt(s) + 1 and source(s) t source(s′ ), where source((s0, s1, . . . , sj), l1, . . . , lm) = sj and dpt((s0, s1, . . . , sj), l1, . . . , lm) = j.
• ˆL is defined as ˆL(s, s′ ) = L(source(s), source(s′ )).

It is easy to see that the unravelling of any GKS is an IBIS. Notice that each IBIS is a GKS, and unravelling of an IBIS results in the same structure. We write ISM to indicate that ISM is the unravelling of the GKS M. In the following we assume that the unravelling of a finite path s1 . . . sn is the structure with the universe {s1, . . . , sn} and the transition relation {(si, sj)|i < j ≤ n}. We write ˆ I to denote the unravelling of a path I on M. Since there is one to one correspondence between paths in M and intervals in ISM, we will often use I and ˆ I interchangeably.

In the rest of the paper we define a number of interval logics L of different expressibility. In this context we are interested in studying the complexity of their model checking problem.

Definition 4. Given a logic L, a GKS M = (S, s0, t,L), a path I = s0s1 . . . sl, and a formula ϕ ∈ L, the model checking problem for L amounts to checking whether or not ISM, ˆ I |= ϕ.

The above defines the problem of model checking generalised Kripke structures against specifications in L. Different logics will have a different syntax and may use a different satisfiability notion, but we will refer to the problem as stated above.

We show that our lower bounds hold even under a strong condition known in interval temporal logic literature as the locality assumption[Moszkowski, 1983]. We say a model M = (S, s0, t,L) satisfies the locality assumption if for all s, s′ ∈ S, L([s, s′ ]) = L([s, s]), that is, the labelling of intervals depends only on the initial point. GKS satisfying the locality assumption can be seen as standard Kripke structures, i.e., Kripke frames paired with an interpretation for the states.

3 Epistemic Interval Temporal Logic

In this section we put forward two epistemic logics for which satisfaction is defined on intervals and not on points. Epistemic Interval Temporal Logic (EIT) is a multi-modal epistemic logic where each operator Ki represents the knowledge of agent i ∈ A. The logic EITC is the extension of EIT to common knowledge over groups G ⊆ A.

3.1 The logics EIT and EITC

We start by defining the syntax for the logics EIT and EITC.

Definition 5. The syntax of EIT is given by the following BNF:

The syntax of EITC is given by the following BNF:

where p ∈ Var is a propositional variable, i ∈ A is an agent, and G ⊆ A is a set of agents.

Formulas built according to Definition 5 are the usual epistemic logics in their static versions with and without common knowledge.

In the following we use the Boolean connectives ∨, ⇒, ⇔ and constants ⊤,⊥ introduced in the standard way. We also use the dual operator for epistemic possibility ¯Ki defined as ¯Kiϕ = ¬Ki¬ϕ. As usual, let EGϕ stand for ∧i∈G Kiϕ and define EiG as E0Gϕ = ϕ and En+1 G ϕ = EGEnGϕ.

We now define when an epistemic formula is satisfied in an interval in an IBIS.

Definition 6 (Satisfaction). Given a formula ϕ ∈ EITC, an IBIS IS, and an interval I, we inductively define whether ϕ holds in the interval I, denoted IS, I |= ϕ, as follows:

• For all p ∈ Var , we have IS, I |= p iff p ∈ L(I).
• IS, I |= ¬ϕ iff it is not the case that IS, I |= ϕ.
• IS, I |= ϕ1 ∧ϕ2 iff IS, I |= ϕ1 and IS, I |= ϕ2.
• IS, I |= Kiϕ, where i ∈ A, iff for all I ′ ∼i I we have IS, I ′ |= ϕ.
• IS, I |= CGϕ, where G ⊆ A, iff for all n ∈ N we have IS, I |= EnGϕ.

The satisfaction definition for EIT is obtained from Definition 6 by omitting the last clause. The key clause in Definition 6 is the one relating to the epistemic modality Ki. Intuitively, agent i knows that ϕ in an interval I if ϕ holds in all intervals I ′ which are epistemically indistinguishable to I, denoted I ∼i I ′ . This is defined by considering all global states in the interval I and ensuring they are pointwise epistemically equivalent to the corresponding states in I ′ . Formally, define as usual [Fagin et al., 1995] that two global states g, g′ are such that g ∼i g′ iff li(g) = li(g′ ), i.e., two global states are epistemically equivalent for agent i if its local states are the same in the two global states. We say that two intervals I = s1, . . . sk, I ′ = s′1 , . . . s′l are such that I ∼i I ′ iff k = l and for all j ≤ k, li(sj) = li(s′ j). In other words an agent i cannot distinguish between the corresponding states in the intervals I, I ′ . This notion corresponds to other concepts in computer science, including the notion of observational equivalence in security [Honda and Yoshida, 1995]. Intuitively, it is the natural extension from local stateequivalence to local path-equivalence in an epistemic setting.

Example 7. Consider the structure from Figure 1 and the interval I = s1s2s3. A formula K1p is not satisfied in I because there is an interval s3s2s3 ∼1 I that is not labelled by p. A formula K1¬K1p is satisfied in I because for all intervals I ′ ∼1 I we have that I ′ ∼1 s3s2s3, so I ′ does not satisfy K1p.

Example 8. Consider a structure containing the states s and t, such that the pair (s, t) is the only one labelled by a propositional variable p. Consider an agent 1 that cannot distinguish any states, i.e., we have u ∼1 u′ for all states u, u′ , and the formula ϕ = ¯ K1p. Formula ϕ is true in an interval of length n iff there is a path from s to t of length n.

3.2 The complexity of model checking GKS against EIT and EITC

In this subsection we show that the model checking problem for EITC can be solved in polynomial space. Then, we show that this bound is tight, proving that the model checking problem is PSPACE-hard, even for the logic EIT on structures satisfying the locality assumption. In Section 5 we discuss interesting fragments of the logic EITC for which better complexity can be shown.

Theorem 9. The model checking problem for the EIT logic is in PSPACE.

Proof. We show an alternating algorithm that solves the problem in polynomial time. Since APTIME = PSPACE, this leads to the membership is PSPACE.

The algorithm solve_eitc(M, I, ϕ) checks whether a formula ϕ is satisfied in an interval I of a model M recursively. In case of a formula of the formKiϕ, the algorithm calls itself universally for all (equivalent) intervals. In case of a formula of the form CGϕ it first computes the equivalence relation corresponding to CG using a standard fixed-point approach, and then proceeds as in the case of Kiϕ.

Algorithm solve_eitc(M, I , ϕ) Output: T rue/F alse

1. If ϕ = p, then if I is labelled by p then return True, else return F alse.
2. If ϕ = ¬ϕ′ , then return not solve_eitc(M, I, ϕ′ ).
3. If ϕ = ϕ1 ∧ ϕ1, then return the logical and between the results of solve_eitc(M, I, ϕ1) and solve_eitc(M, I, ϕ2).
4. If ϕ =Kiϕ′ , then compute solve_eitc(M, I ′ , ϕ′ ) for all intervals I ′ such that I ∼i I ′ . If solve_eitc(M, I ′ , ϕ′ ) returns False for some of them, then return False, else return T rue.
5. If ϕ = CGϕ′ , then compute the smallest equivalence relation ∼G containing all the relations ∼i for i ∈ G,

and then call solve_eitc(M, I ′ , ϕ′ ) analogously to the step above but by considering ∼G in place of ∼i.

Clearly, the algorithm solves the model checking problem and requires only polynomial time.

We show the lower bound for the logic EIT.

Theorem 10. The model checking problem for EIT is hard for PSPACE, even if we consider only structures that satisfy the locality assumption.

Proof. We reduce the quantified Boolean formula (QBF) problem to the model checking for EIT with the locality assumption. For a formula Ψ = Q1p1Q2p2 . . .Qnpn.ρ, where Qi ∈ {∀, ∃} and ρ is quantifier-free, we define a structure M = (S, $, t,L) with the set of states S = {T, $} ∪ {1, . . . , n} × {F, T}. We are interested in intervals of the form $(1, v1)(2, v2) . . . (n, vn), where each vi ∈ {F, T} represents a valuation of pi. The only propositional variable in the model is T , and it labels only intervals starting from T, i.e., all the pairs (T, s). The relation t is such that from $ there is a transition to every other state; from T there is a transition only to T ; from (i, j) there is a transition to (i+1, j ′ ) for any j, j ′ ∈ {F, T}.

We use 2n agents. For i ≤ n, agent i cannot distinguish only between the states (i, T ) and (i, F ), and agent n + i can distinguish two states only if one of them is (i, F).

Consider an interval I = $(1, v1) . . . (n, vn). The formula ¯Kn+iT is satisfied in I iff I ∼n+i T . . . T, that is, by the definition of agent n+i, iff (i, vi) ∼n+i T , that is iff vi = ⊤. Clearly, vi = ⊤ iff I represents an interval in which pi is true.

Let ϕn+1 be a result of replacing in ρ every pi by ¯Kn+iT. By the above observation, an interval I satisfies ϕn+1 iff it represents a valuation that satisfies ρ.

For quantifiers, consider the formula Kiϕ. This formula is satisfied in an interval I = $(1, v1) . . . (n, vn) iff for all j ∈ {F, T}, the formula ϕ is satisfied in $(1, v1) . . . (i - 1, vi-1) (i, j) (i + 1, vi+1) . . . (n, vn), that is, iff ϕ is satisfied at all the intervals that represent the same valuation of propositional variables, possibly except for pi. Similarly, the existential quantifier can be simulated by a formula ¯Kiϕ.

To finish the reduction, we define formulas ϕn, . . . , ϕ1 recursively. If Qi = ∀, then we set ϕi = Kiϕi+1, and otherwise we set ϕi = ¯Kiϕi+1. The above observations show that an interval $(1, F) . . . (n, F) satisfies ϕ1 iff Ψ is true.

We conclude this section by studying the complexity of the satisfiability problem, i.e., whether or not a given formula ϕ admits an IBIS IS and an interval I such that IS, I |= ϕ.

Theorem 11. The satisfiability problem for EIT is PSPACEcomplete; the satisfiability problem for EITC is EXPTIMEcomplete.

Proof. Let S5∗ be a multimodal modal logic interpreted over structures with equivalence relations S1, S2, . . . associated to the modal operators □1,□2, . . . , and S5C∗ be an extension of S5∗ by adding the common knowledge operator. Let f be a bijection that transforms the formulas of EITC by replacing each Ki by □i. We claim that any EIT (resp., EITC) formula ϕ is satisfiable iff f(ϕ) is satisfiable in the logic S5∗ (resp., S5C∗), that is, that f and f -1 are polynomialtime reductions between the satisfiability problems for EIT (resp., EITC) and S5∗ (resp., S5C∗). The complexity of the satisfiability problem for S5∗ and S5C∗ follows from the results for S5m and S5Cm [Halpern and Moses, 1992; Fagin et al., 1995].

Assume that ϕ is satisfied in a model IS = (S, s0, t,L) and an interval I. Consider a Kripke structure M = (W, s0, S1, . . . , Sm, L) such that W consists of the intervals of IS, and for any worlds J , J ′ of M, we have that JSiJ ′ iff J ∼i J ′ in IS. By induction one can see that f(ϕ) is satisfied in the world I in M.

Conversely, assume that a formula f(ϕ) is satisfied in a world w of a model M = (W, w0, S1, . . . , Sm, Π). Assume that M contains only the relations in ϕ. We construct a model IS = (W ∪ {s0}, s0, t,L), where s0 is a fresh initial state. The transition relation t contains an edge (s, t) iff s = s0. For each i, the relation ∼i contains (s0, s0) and all the pairs from Si. So we have ss′ ∼i tt′ iff s = t = s0 and s′Sit′ . We set L(s0, w) = π(w). By induction we can see that ϕ is satisfied in the interval s0w in IS.

The algorithm solving the model checking for EIT (resp., EITC) works as follows. For a given formula ϕ, replace all occurrences of Ki by □i, and check the satisfiability of the resulting formula in logic S5∗ (resp., S5C∗).

4 Epistemic Halpern-ShohamLogic

As discussed, the logic EITC contains no temporal operators. In this section, we enrich EITC by means of interval-based Halpern-Shoham modalities.

The temporal operators in the Halpern-Shoham logic represent temporal relations between intervals as originally defined by Allen [Allen, 1983]. Six of these relations are presented in Figure 2: RA ("after" or "meets"), RB ("begins" or "starts"), RD ("during"), RE ("ends"), RL ("later"), and RO ("overlaps"). Six additional operators can be defined corresponding to the six symmetric relations. Formally, for each X ∈ {A, B, D, E, L, O}, we also consider the relation R ¯X, corresponding to RX -1 .

Definition 12. The syntax of the Epistemic Halpern-Shoham Logic (EHS) is defined by the following BNF.

where p ∈ Var is a propositional variable, i ∈ A is an agent, and G ⊆ A is a set of agents.

Definition 13 (Satisfaction). Given a formula ϕ ∈ EHS, an IBIS IS, and an interval I, we define whether ϕ holds in the interval I, denoted IS, I |= ϕ, by adding the following clause to those reported in Definition 6.

1. M, I |= 〈X〉ϕ iff there exists an interval I ′ such that IRXI ′ andM, I ′ |= ϕ, where RX is an Allen's relation as above.

We often use the operator [G] defined as

which can be read as "in all the (reachable) intervals ϕ holds" and its existential version 〈G〉ϕ = ¬[G]¬ϕ.

Example 14. Consider the structure from Figure 1 and the interval I = s1s2s3. We have IS, I |= [G]¬K1p because each interval labelled by p is of the form s1t1 . . . tns3 (where ti stands for s1, s2, s3 or s4 as appropriate) and agent 1 cannot distinguish it from s1t1 . . . tns1, which does not satisfy p. By contrast, we have IS, I ̸|= [A]K1¬p. Indeed the path I ′ = s3s2s3 is such that IRAI ′ , but I ′ does not satisfy K1¬p since the interval s1s2s3 ∼1 I ′ is labelled by p.

Example 15. Consider a structure containing intervals labelled by propositional variables s and t. The formula

where pi = [B]⊥ is a formula satisfied only in point intervals, states that there is a path from a point-interval satisfying s to a point-interval satisfying t through which Agent 1 knows that safe holds.

Note that we consider tree-like orders, but not necessarily linear, and we allow for point intervals. It is known that over such orders, even the operator 〈D〉 can on its own represent successful runs of Turing machines [Marcinkowski and Michaliszyn, 2011].

4.1 BDE fragment of EHS logic

The undecidability of the satisfiability problem for EHS follows from the undecidability of HS [Halpern and Shoham, 1991]. It is however instructive to identify fragments of EHS that lead to comparatively attractive model checking problems. We here confine ourselves to consider the BDE fragment of EHS logic, i.e., the logic defined in Definition 12 by considering only the clauses for the modalities 〈B〉, 〈D〉, 〈E〉, and Ki and CG. We show the following result.

Theorem 16. The model checking problem for the BDE fragment of EHS is PSPACE-complete.

Proof. The lower bound follows from Theorem 9; so we only show the upper bound. We extend the alternating algorithm from the proof of Theorem 9 by adding the relevant temporal cases. In the case of a formula of the form 〈B〉ϕ, 〈D〉ϕ, or 〈E〉ϕ, the revised algorithm guesses a new interval (resp., prefix, infix of suffix of the current one) and calls itself recursively.

Formally, the algorithm, called solve_ehs, extends the algorithm solve_eitc by the following rules.

1. If ϕ = 〈B〉ϕ′ , then for all k s.t. 1 ≤ k < l compute solve_ehs(M, s1 . . . sk, ϕ′ ). Return True if at least one sub-process returned True.
2. If ϕ = 〈D〉ϕ′ , then for all k, k′ s.t. 1 < k < k′ < l compute solve_ehs(M, sk . . . sk′ , ϕ′ ). Return True if at least one sub-process returned True.
3. If ϕ = 〈E〉ϕ′ , then for all k s.t. 1 < k ≤ l compute solve_ehs(M, sk . . . sl, ϕ′ ). Return True if at least one sub-process returned True.

Clearly, the algorithm requires only polynomial time.

The undecidability of the satisfiability problem for the BDE fragment of EHS follows by the one of the logic containing 〈B〉, 〈D〉, and 〈E〉 only [Bresolin et al., 2011].

5 The Complexity of Some Noteworthy Fragments

In this section we show that some interesting fragments of EHS logic are endowed with an easier model checking problem. We start by defining the knowledge depth of an EHS formula ϕ (denoted KD(ϕ)) as follows.

• KD(p) = 0 where p is a propositional variable.
• KD(ϕ1 ∧ ϕ2) = max(KD(ϕ1), KD(ϕ2)).
• KD(¬ϕ) = KD(〈X〉ϕ) = KD(ϕ).
• KD(Kiϕ) = KD(CGϕ) = KD(ϕ) + 1.

We assume that the reader is familiar with the concept of the polynomial hierarchy [Papadimitriou, 1994].

Theorem 17. The model checking problem for EITC specifications ϕ, such that KD(ϕ) ≤ k for some k ≥ 1, is ∆Pk-1complete.

Proof. (Sketch). The lower bound simply follows by applying the reduction from Theorem 10 to the QBFk-1 problem, that is, the QBF problem restricted to formulae with quantifier depth bounded by k - 1.

The algorithm for the upper bound proceeds as the algorithm for EITC, except for the case of the formulae of the form Kiϕ or CGϕ, where KD(ϕ) = 0. For the case of Kiϕ (resp., CGϕ) with KD(ϕ) = 0, the algorithm first generates the list of all pairs (t1, tl) such that there is an interval I ′ = t1 . . . tl s.t. I ∼i I ′ (resp., I ∼G I ′ , where ∼G is the smallest equivalence relation containing all the relations ∼i for i ∈ G). Then, for each pair (t1, tl) found, it checks whether the knowledge-free formula ϕ is true in an interval labelled by L(t1, tl). The algorithm returns True if at least one is and False otherwise.

What remains to be explained is how to compute, for a given equivalence relation ∼ (which may stand for ∼i or ∼G) and an interval s1 . . . sn, the set of pairs (t1, tn) s.t. there is an interval t1 . . . tn ∼ s1 . . . sn. This can be done in polynomial time by the function find_all defined as follows.

Algorithm find_all (M, ∼, s1 . . . sn) Output: Set of pairs

1. Let R1 := {(t, t)|t ∼ s1}.
2. For each i = 2, 3, . . . , n:
3. Set Ri := ∅.
4. For each (t1, ti-1) ∈ Ri-1:
5. For each state ti such that ti ∼ si, if there is a transition from ti-1 to ti, then add (t1, ti) to Ri.

3. Return Rn.

The algorithm runs in time O(n · |S|3 ), where S is the set of states of M.

The result above does not hold for EHS, as even for formulae of knowledge depth 1 we obtain a ∆1k -hard model checking problem. Below we define a variant whose model checking problem is ∆Pk -complete for formulae of knowledge depth bounded by k.

Definition 18. The syntax of the logic EHSP is defined by the following BNF expression

where p ∈ Var is a propositional variable, i ∈ A is an agent, and G ⊆ A is a set of agents.

Theorem 19. The model checking problem for EHSP specifications ϕ, such that KD(ϕ) ≤ k for some k ≥ 0, is ∆Pk - complete.

Proof. (Sketch). To obtain the lower bound, we modify the reduction given in the proof of Theorem 10 in the following way. We use additional propositional variables 1, . . . , n and label each pair of states of the form ((i, T), s), where s ∈ S by i; for each i < n we also replace the formula ¯Kn+i⊤ with 〈D〉i and ¯K2n⊤ with 〈E〉i. It can be checked that the result then follows.

For the upper bound we extend the algorithm for EITC by the following rule.

1. If KD(ϕ) = 0, then for all subintervals of I and all subformulae of ϕ, determine which of the formulae are satisfied in which subintervals (starting from formulae of smallest modal depth). Return True if I satisfies ϕ and False otherwise.

This step can be performed in time |I|2 · |ϕ|, which is clearly polynomial in size of the input.

It follows that model checking specifications with no knowledge operators is in PTIME.

Finally, we present an NP-complete fragment of EHS.

Definition 20. The syntax of the logic EHS∃ is defined by the following BNF expression.

where p ∈ Var is a propositional variable, i ∈ A is an agent, and G ⊆ A is a set of agents.

Satisfaction for EHS∃ is defined as in Definition 13 by assuming that ¯ CGϕ is an abbreviation for ¬CG¬ϕ.

Theorem 21. The model checking problem for EHS∃ is NPcomplete.

Proof. (Sketch). The lower bound follows by applying the reduction given in the proof of Theorem 10 to existential formulae. We show the upper bound by describing the algorithm solve_ehs∃ which consists of steps 1-3 from solve_eitc to which we add the following:

1. If ϕ = ¯Kiϕ′ , then guess I ′ such that I ∼i I ′ and return the value of solve_ehs∃(M, I ′ , ϕ′ ).
2. If ϕ = ¯ CGϕ′ , then compute the smallest equivalence relation ∼G containing all the relations ∼i for i ∈ G, guess I ′ such that I ∼G I ′ and return the value of solve_ehs∃(M, I ′ , ϕ′ ).
3. If ϕ = 〈X〉ϕ′ , then guess an interval I ′ such that IRXI ′ and return the value of solve_ehs∃(M, I ′ , ϕ′ ).

The algorithm runs in non-deterministic polynomial time.

6 Conclusions and FutureWork

In the Introduction we pointed out that: i) while the satisfaction problem for interval temporal logic has been studied in considerable detail, no results are known for its model checking problem, and ii) while intervals have been used in various areas in computer science, they are still relatively unexplored in AI and MAS. In this paper we firstly put forward a semantics for epistemic modalities in the context of intervals and defined epistemic logics with and without interval operators. We argued that the notion we arrived to is the natural extension to intervals from the point-based epistemic interpretations commonly used in the literature.

Secondly, we introduced the model checking problem for these logics and studied it for a number of cases of interest. We proved that the powerful epistemic logic EITC with individual and common knowledge as well as three interval operators has a PSPACE-complete model checking problem. While we see this as positive result given the expressiveness of EITC, we also identified fragments with better complexity, including PTIME, for logics with a limited number of nested epistemic operators. All the results hold as well for the logics without the common knowledge operator.

In the future we would like to identify the complexity of the model checking problem for the full logic EHS as well as the AB ¯BDELO fragment, i.e., the fragment without past modalities. We are also interested in exploring how compact representations of the type considered in [Lomuscio and Raimondi, 2006] affect the results in this paper and how intervals can be related to clocks in the context of verification [Lomuscio et al., 2007].

Acknowledgements. This research was supported by the EC STREP Project "ACSI" (grant no. 257593).