Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications

1 Introduction

Model checking is the leading technique in verification. Despite its advantages, the number of commercial applications of this technique is still relatively small. This is often explained by the high entry level for model checking specialists - writing appropriate specifications requires a lot of knowledge and, at the same time, a lot of precision. Therefore, for many companies, it is much easier and cost-efficient to perform tests rather than to verify the software. This means that one of the most important challenges for the verification community is to lower the difficulty of performing formal verification. Among many approaches to this problem, one is to use a specification language that treats intervals (processes), rather than time points, as primary objects. It is believed that many important properties are significantly easier to express in terms of intervals and their temporal correspondence than using time points [Lomuscio and Michaliszyn, 2013].

Early attempts to interval-focused verification include the Moszkowski's Interval Temporal Logic [Moszkowski, 1983] and the Propositional Dynamic Logic [Fischer and Ladner, 1979]. The former, however, uses quite a complicated language (one of the main operators allows to split a given interval into two parts, which is quite unreadable), and the latter, while allows for actions that may be seen as intervals, is still essentially point based.

Recently, two lines of research emerged to define a logic for the model checking problem in which intervals are firstclass citizens. First, in [Lomuscio and Michaliszyn, 2013], the Epistemic Halpern-Shoham (EHS) logic was introduced. Not much later, [Montanari et al., 2014] employed the logic HS, later extended with regular expressions [Bozzelli et al., 2017]. Both EHS and HS are based on the Halpern-Shoham The most significant difference, we believe, is the way that both logics treat past events. To exemplify this, consider the following property: if the server is offline, then there was an interval earlier where a warning message was sent. In the EHS setting, every property is considered in an interval with a history, i.e., a computation from the initial state to the beginning of this interval. So, the backward modality "there was an interval earlier" refers to an event that really happened during this computation. In the HS case, on the other hand, there are no histories, therefore this means "it was possible to reach this interval by a computation containing sending a warning". This makes the semantics of HS easier, but also less intuitive.

The other difference between EHS and HS is less fundamental but easier to notice: EHS is defined for multi-agent systems while HS typically considers a single-agent system. Therefore, EHS contains also epistemic modalities, typical for multi-agent systems: Ki ("agent i knows...") and CΓ ("it is common knowledge among the group of agents Γ...").

A lot of research was performed to establish the decidability and complexity status of the model checking problem with HS [Molinari et al., 2015; Bozzelli et al., 2016a; Molinari et al., 2016; Bozzelli et al., 2018a; Bozzelli et al., 2018b; Molinari et al., 2018], as well as its expressibility [Bozzelli et al., 2016b; Goranko et al., 2004]; perhaps the best summary is the Alberto Molinari PhD thesis [Molinari, 2019]. For the whole logic, the model checking problem is decidable, but no elementary upper bound is known. The best known lower bound, on the other hand, is the EXPSPACE lower bound that works for any fragment containing two modalities: "begins with" and "ends with". On the other hand, the decidability status of the model checking against EHS specifications was not known. Here, we show that the model checking problem for EHS is decidable. The obtained complexity is nonelementary, which matches the best known upper bound for a (simpler) logic HS.

To show the decidability, we reduce the problem to the satisfiability problem of the monadic second-order logic on trees (SkS), which is known to be non-elementary decidable. To deal with epistemic modalities, we consider a variant of SkS in which the trees are infinite in both directions, i.e., every node has a predecessor and successors.

To complete the study on the decidability status, we also consider EHS in an LTL-like scenario, where the question of interest is whether all the tracks of a given model satisfy a given EHS formula (that is, once a track is selected, the modalities refer only to intervals within this track). Under such assumptions, the model checking problem is undecidabile even if only epistemic modalities are allowed.

Relatedwork A large number of point-based logics is used in the model-checking scenario, including LTL, CTL, ATL and so on; in some restricted cases, their expressive power matches the expressive power of the logic HS [Bozzelli et al., 2016b]. However, none of them is equivalent (in terms of the expressive power) to the logic EHS.

Two extensions of the Propositional Dynamic Logic are seemingly close to EHS. First one is E-PDL [van Benthem et al., 2006], which adds epistemic modalities to PDL. These modalities, however, are interpreted over points rather than over intervals. The other one is called "PDL with all extras" [Lange, 2006], and allows to use conjunction and complementation with PDL actions. However, the semantics of these operations is still point-based: for example, the action 〈a1 ∧ a2〉 means "there is a path satisfying a1 and there is a path satisfying a2... ", rather than "there is a path satisfying a1 and a2... ", so it cannot be used to express conjunctions of properties of intervals.

2 Interval-Based Interpreted Systems

We assume a set of agents A = {0, . . . , m} to be fixed for the rest of this paper; the agent 0 is often called the environment.

The models we use for verification are called interpreted systems with regular labellings (ISRL). These models are similar to standard Multi-Agent Systems, except that the labelling function is defined on sequences of states rather than single states by means of regular expressions.

Given a family of finite alphabets X = {X0, . . . ,Xm}, the set of regular expressions over X, denoted by REX, is defined by the following BNF expression:

where s is a Boolean combination of conditions i : l, where i ∈ {0, . . . ,m} and l ∈ Xi. We allow parentheses for grouping and often omit the concatenation symbol "·".

A regular expression over X is interpreted over a word whose letters are from the product X0 × · · · ×Xm. The semantics of regular expressions over X is defined in the usual manner, i.e., by a function Lang that for a regular expression returns a language of words accepted by this expression. The only difference is the case of s, where we define Lang(s) to be the set of letters (x0, . . . , xm) such that s is satisfied when we replace each "i : " by "xi =".

The languages definable with such regular expressions are regular, and therefore can be recognized by finite automata.

Example 1. The regular expression (0: a ∨ 1: b)∗ over {{a, b}, {a, b}} defines the language {(c0, d0) . . . (cm, dm) | ∀i.ci = a ∨ di = b}.

The models we study are defined as follows.

Definition 2 (ISRL, [Lomuscio andMichaliszyn, 2016]). An interpreted system with regular labellings (ISRL) is a tuple IS = ({Li, lI i , ACTi, Pi, ti}i∈A, λ), where for each i ∈ A:

• Li is a finite set of local states for agent i,
• lI i ∈ Li is the initial state for agent i,
• ACTi is a finite set of local actions available to agent i,
• Pi : Li → 2ACTi is a local protocol function for agent i, returning the set of possible actions in a local state,
• ti ⊆ Li × ACT × Li, where ACT = ACT0 × · · · × ACTm, is a local transition relation for agent i returning the next local state when a joint action is performed by all agents on a given local state.

Furthermore, λ: Var → RE{L0,...,Lm} is a labelling function, where Var is a finite set of propositional variables.

Paths For an ISRL as above, we define the set of global configurations G as L0 × · · · × Lm, and the initial global configuration lIG as (lI0 , . . . , lIm). The transition relation tG between global configurations is induced by IS as follows: tG((l0, . . . , lm), (l′0 , . . . , l′m)) iff there exists a joint action (a0, . . . , am) ∈ ACT such that for all i we have ai ∈ Pi(li) and ti(li, (a0, . . . , am), l′i ).

A path is a finite sequence g1g2 . . . gk of elements of G such that for each i < k we have tG(gi, gi+1).

For each global configuration g = (l′0 , . . . , l′m) ∈ G and an agent i, by li(g) we denote the local state l′i .

Definition 3 (Model). Given an ISRL IS = ({Li, lI i ,ACTi, Pi, ti}i∈A, λ), the model of IS is a tuple M = (S, sI , t, {∼i}i∈A, λ), where

• S is the set of paths of IS starting in lIG,
• sI = lIG is the (single-state path containing the) initial state of the system,
• t is the transition relation such that t(s1, s2) iff there is a global state g such that s1g = s2 (i.e., the path s1 is the prefix of s2 of length |s2| - 1),
• ∼i⊆ S2 is the epistemic equivalence relation for agent i
• such that g1 . . . gk ∼i g′1 . . . g′ l iff li(gk) = li(g′ l ).
• λ is the labelling function (same as in IS).

We assume that the system is deadlock-free, i.e., for every state there is at least one possible joint action of agents. This assumption is only to make the presentation easier: any system can be easily amended to meet this requirement, e.g., by adding a "sink state". Therefore, the models are labelled infinite unordered trees with the set of nodes S, the root sI, the set of edges t, the labelling λ and epistemic relations ∼i.

For paths p1, p2, we write p1 ⊏ p2 if p1 is a proper prefix of p2 and p1 ⊑ p2 if p1 ⊏ p2 or p1 = p2. An interval is a pair [s, t], such that s, t ∈ S and s ⊑ t. An interval represents a path in a system augmented with a history of states that lead to this path from the initial state of the system. It is worth to note that in a model, s ⊏ t means that t is a descendant of s.

Comment. The definition presented here is essentially equivalent to the one in [Lomuscio and Michaliszyn, 2016]. The main difference is that they defined intervals as pairs (p, ph) such that php is a path from a starting configuration. In our notion, this is represented as [phg, php], where g is the first element of p. We decided to use an alternative representation to make the translation from EHS to MSO on trees easier to present.

3 The Logic EHS

EHS uses twelve temporal operators, defined as in [Halpern and Shoham, 1991]. Six of these relations are presented in Figure 1. The remaining six relations are defined as their inverses: R ¯X = RX -1 . EHS allows also for two kinds of epistemic modalities: Ki for an agent i ("agent i knows") and CΓ for a set of agents Γ ("it is common knowledge in Γ").

Definition 4 (Syntax of EHS). The syntax of EHS is defined by the following BNF.

where p ∈ Var is a propositional variable, i ∈ A is an agent, Γ ⊆ A is a set of agents, and X is one of the HS modalities: A, ¯ A, B, ¯B, D, ¯D, E, ¯E, L, ¯L, O or ¯O.

We use standard abbreviations, including [X]ϕ for ¬〈X〉¬ϕ (universal temporal operator) and the usual Boolean connectives ∨, ⇒, ⇔ and the constants ⊤, ⊥.

Two intervals I, I ′ are indistinguishable for an agent i, denoted as I ∼i I ′ , if they have the same length and the states on corresponding positions are indistinguishable [Lomuscio and Michaliszyn, 2013]. Formally, [s, sg1 . . . gk] ∼i [s′ , s′ g′1 . . . g′ l ] iff k = l, s ∼i s′ and sg1 . . . gj ∼i s′ g′1 . . . g′j for each j ≤ k. Similarly, for a group of agents Γ, we define ∼Γ on states as the transitive closure of (⋃i∈Γ ∼i), and then we extend this to intervals in the same manner.

We now define the satisfaction relation.

Definition 5 (Semantics of EHS). Given an EHS formula ϕ, an ISRL IS, its model M = (S, sI , t, {∼i}i∈A, λ), and an interval I = [g1 . . . gk, g1 . . . gl], the formula ϕ holds in the interval I, denotedM, I |= ϕ, iff one of the following holds:

• ϕ = p and gk . . . gl ∈ Lang(λ(p)),
• ϕ = ¬ϕ′ and it is not the case that M, I |= ϕ′ ,
• ϕ = ϕ1 ∧ϕ2 andM, I |= ϕ1 andM, I |= ϕ2,
• ϕ =Kiϕ, i ∈ A, andM, I ′ |= ϕ for all I ′ ∼i I,
• ϕ = CΓϕ, Γ ⊆ A, andM, I ′ |= ϕ for all I ′ ∼Γ I,
• ϕ = 〈X〉ϕ and there is an interval I ′ such that IRXI ′ and M, I ′ |= ϕ, where RX is a temporal relation.

We write IS, I |= ϕ if M, I |= ϕ, where M is the model of IS, and IS |= ϕ if IS, [sI , sI ] |= ϕ.

The problem of model checking ISRL against EHS specification is defined as follows: given an ISRL IS and an EHS specification ϕ, decide whether IS |= ϕ.

3.1 Example

Consider a bit transmission protocol, where an agent Sender wants to deliver a single bit message to an agent Receiver via a faulty communication channel, modelled using Environment. Assume that the Sender first computes the bit (which is modelled as a non-deterministic choice of the bit), and then repeatedly tries to send the bit. Sending the bit requires three actions (not necessarily happening immediately one after the other): opening the communication channel, sending the bit and closing the communication channel. For each i ∈ {0, 1} being the possible value of the bit, we consider two labellings: λ(si) matching the intervals starting with opening the communication channel, ending with closing the communication channel and sending the bit i during the interval, and λ(ri) matching in every state (point interval) where the bit to be sent is chosen and its value is i.

In this scenario, we can verify whether, for example:

• [G](KReceiverr0 → 〈¯L〉s0) - if Receiver knows that the value of the bit is 0, then it means that Sender has sent 0.
• [G](s0∨s1) ⇒ [O](¬s0∧¬s1) - sending actions do not overlap.
• [G]〈L〉KReceiver(r0 ∨ r1) - it is always possible that Receiver will eventually know the value of the bit.

where [G]ψ = [A]ψ ∧ [L]ψ, interpreted in [sI , sI ], means "globally". For more examples, please refer to [Lomuscio and Michaliszyn, 2013; Lomuscio and Michaliszyn, 2014] and [Lomuscio and Michaliszyn, 2016].

4 Decidability of Model Checking

The infinite tree of degree k is, as usual, a connected structure with a single root such that each node has exactly k (ordered) successors, and every node has a single predecessor except for the root that has no predecessors. The doubly-infinite tree of degree k is a connected structure such that each node has exactly k (ordered) successors, and every node has a single predecessor (e.g., the set of the integers with the successor relation is the doubly-infinite tree of degree 1).

To show the decidability, we reduce the model checking problem to the satisfiability problem of SkS∞ (where k is the degree of the models of a given IS), the Monadic SecondOrder Logic on the doubly-infinite tree of degree k. To show that SkS∞ is decidable, we use the decidability of SkS, the Monadic Second-Order logic on infinite trees of degree k. Below we define SkS∞ and SkS.

Syntax Terms of SkS are formed out of individual (firstorder) variables x, y, z, etc., the empty string ϵ, and right concatenation with 1 . . . k. Atomic formulas are of the form w = w′ , w < w′ and w ∈ X, where w, w′ are terms and X is a (second-order) variable. Formulas are built from atomic formulas using the logical connectives ∧ , ∨, ⇒, ¬ and the quantifiers ∃, ∀ of both individual and second-order variables. The syntax of SkS∞ is the same.

Semantics SkS is interpreted over the infinite tree of degree k; individual variables are interpreted as nodes of the tree and second-order variables are interpreted as sets of nodes. The concatenation xi, for i ∈ {1, . . . , k} is interpreted as the ith successor of the interpretation of x. We define a relation succ(x, y) that holds if y is a successor of x; then, the inequality < is interpreted as the transitive closure of succ. Inclusion and equality of sets, are definable in SkS in an obvious way. The semantics of SkS∞ is the same except that it is interpreted over the doubly-infinite tree of degree k. This semantics can be extended to formulas with free variables and labelled trees in the usual manner.

The decidability (of the satisfiability problem) for SkS was shown in [Rabin, 1977]. Here we show that SkS∞ is also decidable with the same complexity.

Theorem 6. There are polynomial time reductions from SkS to SkS∞ and from SkS∞ to S(k + 1)S.

The reduction from SkS to SkS∞ is straightforward - we can express that there exists a second-order variable Root with exactly one element and relativise the formula so that each quantifier ignores the nodes above this element. The other reduction uses the k + 1th successor of the root to simulate its predecessor, and then repeats it for the predecessor and so on. Then, another relativisation is needed to remove unused k + 1th successors. It turns out that the successor relations and the relation < can be expressed in this encoding.

4.1 Proof Overview

For a given ISRL IS, its model M and an EHS formula ϕ, our goal is to construct an SkS∞ formula Ψ such that Ψ is satisfiable iff IS |= ϕ. Since checking the former is decidable, the decidability of the latter follows.

We will present the construction of the formula Ψ in three steps. Here we give a simplified description of these steps:

Step 1 We construct a formula ΦIS whose models, viewed as unordered trees, have a clearly-marked substructure isomorphic with M without the relations ∼i. For any model of ΦIS, let h be the isomorphism from this substructure to M. Notice that we cannot express the relations ∼i because SkS∞ with binary predicates is undecidable.

Step 2 We show that the formulas of EHSwithout epistemic modalities can be translated to SkS∞: for every EHS formula ϕ, we construct an SkS∞ formula Ψ(x, y) such that ΦIS ∧ Ψ(v, v′ ) holds for some nodes v, v′ if IS, [h(v), h(v′ )] |= ϕ (this part is the reason for the alternative definition of the semantics, as commented in Section 2).

Step 3 We extend the translation to cover epistemic modalities. This is more technical, so we discuss this using an example. Assume that the upper tree in Figure 2 represents a model of IS and that s0 ∼1 s4, s1 ∼1 s5, s2 ∼1 s6 and s3 ∼1 s7. Consider the formula K1ϕ. A naive approach is to try to write an SkS∞formula with variables x, y that states "for all x′ , y′ such that the paths from x to y and from x′ to y′ have the same length and their corresponding states are indistinguishable for agent 1, ϕ (translated to SkS∞) holds". The logic SkS∞ is too weak to express this.

To perform Step 3, we actually need a stronger version of the constructions mentioned in Steps 1-2 that allows us to "reroot" the tree. We assume that the formulas are parametrised by a "current root", which defines a subtree isomorphic with the model of IS. Then, to deal with an epistemic modality, we allow to move the root and relabel the whole tree (using fresh second-order variables) such that in the relabelled tree, an indistinguishable interval ([s4, s7] in our example) is in the same place as the interval [x, y,] ([s0, s3] in our example). The construction guarantees that both intervals have the same length and their relative states are indistinguishable as required. By using universal quantifiers of SkS∞ we can check all relevant intervals.

Notice that indistinguishable intervals can have very long histories; this is why we use doubly-infinite trees - to make sure that we have room to include the whole history. Alternative approaches to this problem are possible, but we found this solution the most elegant.

4.2 Representing aModel

Fix an ISRL IS = ({Li, lI i ,ACTi, Pi, ti}i∈A, λ) and its model M. Assume that the maximal number of successors of a global state in M is k. Let G and tG be as above and let G = {g0, . . . , gn} be an enumeration of all global states. We treat each gi as a second-order predicate. By Gsubstructure of a model N we denote the substructure of N

consisting of all the elements satisfying any of gi. We define an SkS∞ formula modelIS, whose G-substructure, viewed as an unranked tree, is isomorphic with M. The formula modelIS(r, g0, . . . , gn) (where r is an individual variable and gi are second-order variables) is the conjunction of the following formulas.

• g0(r) - the root r is the initial state of M.
• ∀x(∨g∈G g(x) ∧ x ̸= r) ⇒ x > r ∧ ∀y.succ(y, x) ⇒ ∨g∈G g(y) - the G-substructure is a tree rooted in r.
• ∀x ∧g,g′∈G|g̸=g′ ¬(g(x) ∧ g′ (x)) - no node is labelled by two different gs
• ∀x,y,z.succ(x, y)∧succ(x, z)∧y ̸= z ⇒ ∧g∈G(g(y) ⇒ ¬g(z)) - no node has two successors labelled by the same g.
• ∧(g,g′ )̸∈tG ∀x∀y.succ(x, y) ⇒ ¬g(x) ∨ ¬g′ (y) and ∧(g,g′ )∈tG ∀x.g(x) ⇒ ∃y(succ(x, y) ∧ g′ (y)) - the successors in the G-substructure of a state satisfying g are exactly {g′ | tG(g, g′ )}, i.e., the successors of g.

The construction guarantees the following.

Lemma 7. Let IS be an ISRL and M be its model of degree k and global states {g0, . . . , gn}. The SkS∞ formula modelIS(r, g0, . . . , gn) is satisfiable, and if T is its model, then the {g0, . . . , gn}-substructure of T viewed as an unranked tree is isomorphic with M.

4.3 Translation of Formulas

Hereafter we abbreviate g0, . . . , gn to ⃗g. We inductively define an "EHS to SkS∞" translation ets.

We start by defining the translation function for p being a propositional letter. This can be done in a standard way - we transform the regular expression λ(p) into an automaton, and then write a formula that labels the path from x to y with the states of the automaton, starting from an initial one and ending with a final one.

Conjunction and negation are translated directly. For any EHS formulas ϕ, ϕ′ , we define:

• ets¬ϕ(x, y, r,⃗g) = ¬etsϕ(x, y, r,⃗g)
• etsϕ∧ϕ′(x, y, r,⃗g) = etsϕ(x, y, r,⃗g)∧etsϕ′(x, y, r,⃗g)

We now proceed to definition of translation function for temporal relations. Define ets〈X〉ϕ(x, y, r, ⃗g) as:

• ∃zy ≤ z ∧ etsϕ(y, z, r, ⃗g) if X = A,
• ∃zr ≤ z ≤ x ∧ etsϕ(z, x, r, ⃗g) if X = ¯ A,
• ∃zx ≤ z < y ∧ etsϕ(x, z, r,⃗g) if X = B,
• ∃zy < z ∧ etsϕ(x, z, r, ⃗g) if X = ¯B,
• ∃zx < z ≤ y ∧ etsϕ(z, y, r,⃗g) if X = E,
• ∃zr ≤ z < x ∧ etsϕ(z, y, r, ⃗g) if X = ¯E.

The translation for remaining temporal operators is defined in a similar way. Notice that so far we never modify r and ⃗g, and therefore the construction would work also in SkS.

Now we discuss epistemic modalities (Step 3). For every i ∈ A define ∼i⊆ G2 as g ∼i g′ iff li(g) = li(g′ ). Similarly, for every Γ ⊆ A define ∼Γ⊆ G2 as the transitive closure of ⋃i∈Γ ∼i. Since ∼i is just ∼{i}, it is enough to define the transition function for epistemic modalities of the form CΓ, where Γ ⊆ A.

where equivΓ states that r′ , ⃗ g′ give a model in which the interval [x, y] is indistinguishable for Γ with the interval [x, y] in the model given by r,⃗g. Formally, equivΓ(x, y, r, ⃗g, r′ , ⃗ g′ ) is defined as:

4.4 Correctness of the Construction

We show that the construction is correct.

Lemma 8. Let IS be an ISRL with the model M and ϕ be an EHS formula. Let N be a model of modelIS(r, ⃗g) and h be the isomorphism from M to {g0, . . . , gn}-substructure of N. For every interval [s, t] in M we have M, [s, t] |= ϕ iff etsϕ(h-1 (s), h-1 (t), r, ⃗g) holds in N.

Recall that the isomorphism exists due to Lemma 7. The proof goes by induction and is omitted due to the page limit. The main result follows:

Theorem 9. Model checking ISRL against EHS specifications is decidable.

Proof. For an ISRL IS and an EHS formula ϕ, the model checking amounts to constructing the formula

and checking whether this formula is satisfiable (which is equivalent to being true as it has no free variables). It follows from Lemma 8 that this formula is satisfiable iff M, [sI , sI ] |= ϕ, because h(sI ) = r for any isomorphism h defined as in Lemma 7.

The resulting complexity is non-elementary. However, SkS and SkS∞ are elementary when the number of quantifiers alternations is bounded. Therefore, a better complexity can be obtained, if needed, by considering EHS formulas with bounded alternation depth.

5 LTL-like Semantics Leads to Undecidability

In a sense, the way that the intervals are quantified in EHS is similar to CTL: a single formula may depend on different branches of computation. An alternative, LTL-like, approach would be to consider the specification over each possible computation separately. More precisely, for a given ISRL IS and its model M, a trace is an infinite path in the tree M starting in the root. By traces(IS) we denote the set of all such traces.

We adjust the definition of the semantics of EHS (Definition 5) to traces in a straightforward way: each time the semantics refers to an interval, it has to be an interval in this particular trace. We define IS |=LTL ϕ iff for all

Figure 3: An example of an interval encoding a computation of a Turing machine (states of agent 3 are omitted for readability).

T ∈ traces(IS) and all the intervals [sI , t] (i.e., starting from the initial state) we have T, [sI , t] |= ϕ.

Just like LTL is computationally harder than CTL, the LTLlike semantics makes EHS harder.

Theorem 10. For an ISRL IS and an EHS formula ϕ, checking whether IS |=LTL ϕ is undecidable, even if ϕ contains only epistemic modalities.

Proof. We reduce the boundedness problem for Turing machines. We assume a Turing machine M with the alphabet Σ including the letter B (blank), set of states Q, a single initial state q0, and a transition function δ : Σ×Q → Q×Σ×{L, R} such that M starts with the empty tape. A machine M is bounded iff M visits only finitely many configurations during its computations. It is well known that checking if such a machine is bounded is undecidable.

We construct an ISRL IS and a formula ϕ such that there is a trace T of IS and t such that T, (sI , t) |= ϕ iff M is bounded. This implies that IS |=LTL ¬ϕ iff M is not bounded, thus the undecidability.

We use an abbreviation ̂Ki defined, for each agent i, as ̂Kiψ = ¬Ki¬ψ. Notice that ̂Kiψ means "there is an interval indistinguishable for i from the current one that satisfies ψ".

We use four agents: 0 with states {1s, 1, 1e, 2s, 2, 2e,-}, 1, 2 with states S = Σ ∪ (Q × Σ) ∪ {-}, and 3 with a single state -. All the agents have a single action a that is allowed in every state and allows to move from any state except - to any state; from - an agent can move only to -.

The idea is that the interval that satisfies ϕ will encode the initial configuration of M, and we will require that for each configuration, there is an interval (somewhere in the trace, not necessary below the current interval) encoding the next configuration. We will also stipulate that there are only finitely many configurations, which means that M is bounded.

First, we define the labelling λ(I) = (1: (q0,B))(1: B)∗ - it labels the intervals where the states of the agent 1 encode the initial configuration. We will also employ λ(ai) defined as (0: is)(0: i)∗ (0: ie) for i ∈ {1, 2}. We will call intervals matching λ(ai) i-blocks; blocks will be used to encode configurations (e.g., Figure 3 contains three blocks). Furthermore, let λ(end) be defined by ⊤∗ (0: -∧1: -∧2: -)⊤∗ .

So far, we can express the following: the interval encodes the initial configuration in the states of agent 1 and there are only finitely many configurations: a1 ∧ I ∧ ̂K3end.

It remains to express that if there is an interval expressing a configuration, then there is an interval expressing the next configuration. To do this, we need two more labellings.

Let ¯1=2 and ¯2=1. For i ∈ {1, 2}, let the labelling λ(nexti) match the intervals matched by ai where the states of agent 1 and the states of agent 2 describe a configuration (contain exactly one pair (q, a) in each case) and the configuration described by the states of ¯i is the configuration following the configuration described by the states of i. This can be expressed as a regular expression in standard way.

Let ψi = ai ⇒ ̂K¯i(a¯i ∧ next¯i) be a formula for every iblock there is an¯i-block I ′ such that the configuration stored by agent ¯i is the same in both cases. Moreover, because of next¯i, the states of i in I ′ encode the next configuration.

Finally, we define ϕ = a1 ∧ I ∧ ̂K3end ∧ K3(ψ1 ∧ ψ2).

If M visits only a bounded number of configurations, then we can easily construct a trace satisfying ϕ that contains all these configurations and then all the states are triples (-,-,-). On the other hand, if there are a trace T and an interval I that satisfy ϕ, then T contains finitely many configurations including the initial one. By ψ1 and ψ2, T contains all the configurations that M visits, meaning that M visits only a bounded number of configurations.

A similar question: does T, [sI , sI ] |= ϕ for all T ∈ traces(IS) (as in the definition of IS |= ϕ), is also undecidable, but only if we also have at least one modality among {A, ¯ A, ¯B, ¯D, ¯E,L, ¯L}. Otherwise, the model checking is decidable, as only point intervals are reachable from the initial interval. Interestingly, LTL-like model checking EHS without epistemic modalities is decidable [Bozzelli et al., 2016b].

6 Conclusions

We showed that the model checking problem for EHS is decidable in non-elementary time. The only known lower bound is EXPSPACE. The problem of establishing the precise complexity, however, remains open and is hard to predict. On the one hand, the non-emptiness problem of regular expressions with complementation is TOWER-complete, and EHS can express regular expressions and negation; however, the proof of the non-elementary lower bound for regular expressions with complementation alternates complementation and Kleene star, and it does not seem to be possible to do this in EHS. On the other hand, even for a simpler logic, HS, no elementary algorithm is known.

We also showed that LTL-like semantics combined with epistemic modalities on intervals lead to undecidability. The undecidability of the satisfiability problem for EHS without temporal modalities can be shown in the same way.

Acknowledgements

The first author was supported by Polish National Science Centre grant 2014/15/D/ST6/00719. The second author was supported by Polish National Science Centre grant 2016/21/B/ST6/01444.