Model Checking Multi-Agent Systems against LDLK Specifications

1 Introduction

Linear Dynamic Logic (LDL) has recently been put forward as an attractive logic for reasoning about processes [Vardi, 2011]. LDL extends Linear Temporal Logic [Pnueli, 1977] by replacing the linear temporal operators with regular expressions in a way that is similar to that of Propositional Dynamic Logic [Fischer and Ladner, 1977]. From the theoretical point of view, LDL is attractive because it can express all ω-regular properties and is therefore equivalent to monadic second-order logic [Vardi, 2011]. From an application point of view the expressiveness of LDL has been positively evaluated in a number of contexts, including monitoring business processes [De Giacomo et al., 2014]. A major feature of interest in LDL is the fact that its model checking problem is in PSPACE [Faymonville and Zimmermann, 2015]. So while LDL is considerably more expressive than LTL, their model checking problem has the same complexity.

While much progress has been made recently on LDL, including an analysis of the synthesis problem on infinite and finite traces [De Giacomo and Vardi, 2015; 2016], from an agent perspective we highlight two apparent limitations.

Firstly, from a theoretical standpoint, while LDL can express sophisticated temporal or action properties, no proposal has so far been made to augment it with modalities to represent the agents' mental states. This has been conducted successfully for a range of temporal logics in the context of epistemic logic and has resulted in the specification languages LTLK [Fagin et al., 1995] and CTLK [Penczek and Lomuscio, 2003] which have attracted interests both in theory and applications. Due to the expressiveness of LDL the same exercise could be of even higher significance in this context.

Secondly, from an application point of view, no practical algorithm nor toolkit exists for verifying systems against LDL specifications. Indeed, while the computational complexity of the logic has been explored, no symbolic model checking algorithm has so far been put forward. Yet symbolic toolkits [Gammie and van der Meyden, 2004; Kacprzak et al., 2008; Lomuscio et al., 2015] are essential for verifying prototype designs in multi-agent systems.

In this paper we attempt to make a contribution addressing these two aspects. Firstly, in Section 2, we define LDLK, an extension of LDL with knowledge operators, including common knowledge, and its semantics. In Section 3 we put forward a model checking algorithm for verifying multi-agent systems against LDLK specifications. A key feature of the approach is that the procedure is based on alternating automata and amenable to symbolic implementation. In Section 4 we present MCMASLDLK, a model checker for verification of multi-agent systems against LDLK specifications. MCMASLDLK extends the open-source model checker MCMAS, by implementing the algorithm of Section 3 for LDLK. We show the attractiveness of the experimental results obtained and conclude in Section 5.

Related Work. The verification algorithm we introduce for model checking multi-agent systems against LDLK is inspired by the one put forward in [Faymonville and Zimmermann, 2015], which showed that determining satisfiability of parametric LDL specifications is in PSPACE. However, their construction is focused on showing decidability as opposed to practical implementation; specifically, the algorithm does not explicitly address how to handle a potentially unbounded number of ϵ-paths when trying to quantify over all prefixes of a path. The construction we introduce here includes a mechanism for limiting the paths being considered. Our approach is not polynomial space as we eagerly build the automata; but, as we show, still leads to an efficient symbolic implementation in cases of practical interest we tested. Additionally, [Faymonville and Zimmermann, 2015] does not support epistemic specifications and no implementation is put forward.

Our implementation is based on the open-source model checker MCMAS [Lomuscio et al., 2015]. However, MCMAS currently only supports CTLK; LDLK significantly extends the range of specifications supported. Note also that CTLK is implemented in MCMAS by a traditional labelling algorithm. Instead, we here use alternating automata, which are then converted to symbolic B¨uchi automata by using the symbolic breakpoint construction from [Bloem et al., 2006]. So, while MCMASLDLK shares with MCMAS the libraries for parsing the input and constructing some intermediate structures, the verification algorithm is entirely different.

MCMAS has also been extended to address the problem of verifying strategic ability in multi-agent systems; support has been developed for ATL and SL, extended with suitable epistemic operators [Cerm´ak et al., 2014]. However, our work is focused on improving temporal expressivity (as opposed to additional modalities).

The model checker NuSMV [Cimatti et al., 1999] supports a fragment of Property Specification Language (PSL) which, like LDL, can express all ω-regular properties [Cimatti et al., 2006]. However, this is limited to properties also expressible in LTL or CTL. We are not aware of any open-source model checker supporting full PSL.

The model checker MCK [Gammie and van der Meyden, 2004] supports the verification of CTL*K properties. Differently fromMCMAS which is limited to observational semantics, MCK also supports clock semantics and perfect recall (for one agent only). However, CTL*K and LDLK have incomparable expressivity (the ability of CTL*K to reason temporally about a specific path is similar to that of LTL, which cannot express parity [Wolper, 1981]); so the functionality of MCK is different from that of MCMASLDLK.

2 Linear Dynamic Logic with Knowledge

Interpreted systems, introduced in [Fagin et al., 1995], provide a formalism for reasoning about temporal and epistemic properties of MAS. In the approach given in [Lomuscio et al., 2015], agents have locally defined transition relations, and the global transition relation of the system results from the composition of these. We take A = {1, . . . , n} as a set of agents, and e as a special agent called the environment.

Definition 1 (Interpreted Systems). An interpreted system is a tuple IS = 〈{Li, Acti, Pi, τi}i∈A∪{e}, I, h〉, where:

• Li is a finite set of possible local states of agent i.
• Acti is a finite set of possible actions of agent i.
• Pi : Li → 2Acti \{∅} is a local protocol for agent i, specifying which actions agent i can execute from each local state.
• τi : Li×Act1×. . .×Actn×Acte →Li is a local transition function, returning the next local state of agent i following an action by all agents and the environment. We assume agents' actions are consistent with their protocols; i.e., if l′i = τi(li, a1, . . . , an, ae) then for each i ∈ {1, . . . , n}, we have that ai ∈ Pi(li).
• I ⊆ L1×. . .×Ln×Le is the set of initial global states.
• h : AP → 2L1×...×Ln×Le , where AP is a set of atomic propositions, is a valuation function identifying

the global states in which each atomic proposition holds.

We define the global transition relation T to be the composition of the τi, and the set of global reachable states G ⊆ L1 × . . . × Ln × Le to be the set of states reachable through zero or more applications of T on I. We also define an evolution path for IS, as an infinite sequence of global states g0, g1, . . . such that for every i, gi ∈ G, and if i > 0 then there exists actions a1, . . . , an, ae such that for every local state l′j in gi, l′j = τj(lj, a1, . . . , an, ae) for each possible agent j ∈ A ∪ {e} (where lj is the local state of agent j in state gi-1). Furthermore, we denote with π(k) the k-th state of a path π = g0, g1, . . ., and with πk the k-th suffix of a path π; i.e., πk = gk, gk+1, . . .. We also define, for each agent i ∈ A a projection operator li : G → Li which returns the local state of agent i in a given global state.

We now introduce Linear Dynamic Logic with Knowledge (LDLK) by augmenting LDL with epistemic operators.

Definition 2 (LDLK Syntax). An LDLK formula φ is constructed by the following grammar:

where p is a propositional atom, i ∈ A ∪ {e} an agent, Γ ⊆ A ∪ {e} a set of agents and ψ a formula free of dynamic modalities (〈ρ〉φ). We allow the standard abbreviations from propositional logic, and define [ρ]φ = ¬〈ρ〉¬φ.

LDLK enables us to express LDL specifications in an epistemic setting; these are not expressible in LTLK, CTLK, nor CTL*K. In the context of the train gate controller scenario [van der Hoek and Wooldridge, 2002], these include:

• Specifications involving parity, as in "At even states in the run, train 1 is in the tunnel.": [(⊤;⊤)∗ ]tun1;
• Specifications involving alternating sequences, as in "It is common knowledge between the trains that they will alternately occupy the tunnel until one breaks down.": C{1,2}[(tun1; tun2)∗ ](break1 ∨ break2);
• Looping constructions, as in "Until train 2 knows train 1 will eventually enter the tunnel, train 2 stays outside the tunnel; once it knows this, train 2 enters the tunnel.": [(¬K2〈⊤∗ 〉tun1?; ¬tun2)∗ ; K2〈⊤∗ 〉tun1?]tun2;
• Complex regular properties, as in "When train 1 enters the tunnel, it leaves within one step; the controller then knows that the tunnel is intermittently occupied until train 1 re-enters.": [⊤∗ ](tun1 → 〈(⊤ + ⊤?); ¬tun1〉(KC [(tun1 ∨ tun2; ⊤)∗ ]tun1));
• Complex combinations of epistemic operators and regular expressions, as in "The controller knows that after the tunnel is empty for two rounds, the trains will both know that the controller breaks in an odd number of rounds.": KC [⊤∗ ; (empty; empty)]E{1,2}〈⊤; (⊤; ⊤)∗ 〉breakC .

None of the properties above is expressible in CTL*K. As previously mentioned, LDL has been employed in a variety of applications including business processes [De Giacomo et al., 2014]. By combining LDL with epistemic logic we obtain a very expressive language for expressing MAS specifications.

We now define the satisfaction relation.

Definition 3 (Satisfaction). Consider the interpreted system IS = 〈(Li, Acti, Pi, τi)i∈A∪{e}, I, h〉 and let π be a path.

• IS, π |= p iff π(0) ∈ h(p).
• IS, π |= ⊤.
• IS, π |= ¬φ iff it is not the case that IS, π |= φ.
• IS, π |= φ1 ∧ φ2 iff IS, π |= φ1 and IS, π |= φ2.
• IS, π |= Kiφ iff for every state g ∈ G if li(g) = li(π(0)), then IS, g |= φ.
• IS, π |= EΓφ iff for every state g ∈ G if li(g) = li(π(0)) for some agent i ∈ Γ then IS, g |= φ.
• IS, π |= DΓφ iff for every state g ∈ G if li(g) = li(π(0)) for all agents i ∈ Γ then IS, g |= φ.
• IS, π |= CΓφ iff for every state g ∈ G if g1, . . . are states such that li(g) = li(g1), lk1 (g1) = lk1 (g2), . . ., lj(gn) = lj(π(0)) for some agents i, j, k1, . . . ∈ Γ and positive integer n, then IS, g |= φ.
• IS, π |= 〈ρ〉φ iff there exists some i ≥ 0 such that (0, i) ∈ R(ρ, π) and IS, πi |= φ.

The relation R ⊆ (ρ × π) × (N × N) is inductively defined:

• R(ψ, π) = {(i, i +1) : πi |= ψ}
• R(φ?, π) = {(i, i) : πi |= φ}
• R(ρ + ρ′ , π) = R(ρ, s) ∪ R(ρ′ , s)
• R(ρ; ρ′ , π) = {(i, j) : ∃k s.t. (i, k) ∈ R(ρ, π)∧(k, j) ∈ R(ρ′ , π)}
• R(ρ∗ , π) = {(i, i)}∪{(i, j) : ∃k s.t. (i, k) ∈ R(ρ, π)∧ (k, j) ∈ R(ρ∗ , π)}

As in LTL, for a global state g ∈ G, we say IS, g |= φ iff on every path π starting at g we have IS, π |= φ.

Note that, as in mainstream approaches, we here adopt observational semantics for epistemic modalities; intuitively, agents' knowledge is defined on their local state only.

In LDLK the path expressions ρ in the dynamic modalities behave similarly to constructs from PDL:

• ψ checks if the formula ψ (by definition not containing dynamic modalities, but possibly containing epistmic ones) holds at the current state.
• φ? checks if the LDLK formula φ holds at the current state. Unlike ψ, though, the evaluation of φ? does not "progress" along the path - that is, in a composition like φ?; ρ we are checking that φ is true in this state, and that the path from this same state satisfies ρ.
• ρ + ρ′ models the nondeterministic selection between two path expressions; it checks whether either of the path expressions ρ or ρ′ is satisfied by this path.
• ρ; ρ′ models the sequential composition of two path expressions; it checks whether it is possible for the current path to satisfy ρ and then ρ′ .
• 〈ρ∗ 〉 models zero or more instances of ρ, similarly to Kleene star for regular expressions.

Given the above, the intuitive meaning of 〈ρ〉φ is that there exists some prefix matching ρ, after which φ holds; the dual [ρ]φ holds iff after every prefix matching ρ, φ holds.

Given an interpreted system IS, a state g and an LDLK formula φ, the model checking problem involves determining whether IS, g |= φ.

3 Symbolic Model Checking LDLK

We now introduce an approach for verifying an interpreted systems IS against an LDLK specification φ. This is reported in Algorithm 1. As we show below, we have that IS |= φ iff I and the set of states returned by Algorithm 1 on ¬φ are disjoint. Since steps 3 and 4 follow established techniques, we here report steps 1 and 2 only.

Algorithm 1 Symbolic LDLK Model Checking Algorithm

1. Recursively descend φ and construct an LDL formula φ′ that holds in the same states as φ in IS.
2. Construct an alternating automaton for φ′ , encapsulating an accepting run.
3. Convert the alternating automaton to a symbolic B¨uchi automaton via the constructions in [Bloem et al., 2006].
4. Build the product of the B¨uchi automaton and IS; find states admitting an accepting run [Burch et al., 1990].

Translating LDLK to LDL. Given an LDLK formula, we first determine the states in which any epistemic subformulae hold, and introduce fresh atomic propositions holding in precisely the same states. This involves recursively computing the states in which the formula for which we are evaluating knowledge holds, and then using the bottom-up labelling algorithm presented in [Raimondi and Lomuscio, 2004]. The construction always terminates, since formulae are of finite size and thus have a finite nesting depth.

For example, to translate the LDLK formula φ = 〈(Ka(r)? + Kb(q)?); (Kb(q)? + Kb(p)?); ⊤〉Ka(r) we first determine the states in which Ka(r), Kb(q) and Kb(p) each hold. We then define α, β and γ to hold in the respective sets of states, and obtain the formula φ′ = 〈(α?+β?); (β?+ γ?); ⊤〉α, which in our model holds in the same states as φ.

Constructing the Alternating Automaton. Our approach builds upon the construction given in [Faymonville and Zimmermann, 2015] for constructing an alternating automaton that accepts the path π if and only if IS, π |= φ. Given an LDL formula φ, resulting from the translation above, we first convert it into negation normal form (NNF), so that all negations appear before atomic propositions.

The translation of φ (in NNF) to an alternating automaton then largely follows that in [Faymonville and Zimmermann, 2015]. The propositional cases are straightforward. For each dynamic modality 〈ρ〉ψ or [ρ]ψ in φ, we use an extension of Thompson's construction [Thompson, 1968] to build a nondeterministic finite automaton with silent ϵ moves (ϵ-NFA).

We adopt their definition of marked ϵ-NFA.

Definition 4 (Marked ϵ-NFA). A marked ϵ-NFA is a tuple A = (Σ, S, s0 , R, f, m) where Σ is an alphabet, S is a finite nonempty set of states, s0 is an initial state, f is an accepting state, R : (S×(Σ∪{ϵ})) → 2S is a (partial) transition function and m : S → φ is a (partial) marking function assigning LDL formulae to states. Further to the above, if π = s0 . . . sn is a path in a marked ϵ-NFA, we define the markings over π, m(π) = {m(si) | i ∈ {0, . . . , n}}. In our usage, we build marked ϵ-NFAs for each dynamic modality 〈ρ〉ψ or [ρ]ψ in the formula we are checking; the marking function is concerned with tests appearing in the relevant ρ. The overall Having constructed the ϵ-NFA, we convert it into an alternating automaton; to do so, we need to remove any ϵtransitions as these cannot feature in alternating automata.

To do so, [Faymonville and Zimmermann, 2015] constructs a transition relation for the alternating automata that features a disjunction or a conjunction over all possible ϵ-paths. This may lead to difficulties in any resulting implementation as the number of ϵ-paths can be unbounded (in cases where we have a cycle of ϵ-paths, such as (p?)∗ ). To avoid this problem, we introduce the novel notion of critical sets which give us a principled way of capturing only the subset of the ϵ-paths that actually need to be considered. The key intuition behind critical sets is that we only need to consider the "best case" sets of tests to match ρ for 〈ρ〉φ, or the "worst case" for [ρ]φ.

Definition 5 (Marking Sets). Let s, s′ be nodes in a marked ϵ-NFA A = (Σ, S, s0 , R, f, m). M ⊆ range(m) is a marking set from s to s′ if there exists an ϵ-path π from s to s′ in A, such that m(π) = M. We say that π induces M.

Definition 6 (Critical Sets). Let s, s′ be nodes in a marked ϵ-NFA A = (Σ, S, s0 , R, f,m). M is a minimal critical set of the markings range(m) from s to s′ , if M is a marking set from s to s′ , and there does not exist M ′ ⊆ range(m) such that M ′ ⊂M and M ′ is a minimal critical set from s to s′ .

The maximal critical set is defined dually; M is a maximal critical set of range(m) if M is a marking set from s to s′ , and there does not exist M ′ ⊆ range(m) such that M ⊂ M ′ andM ′ is a maximal critical set from s to s′ .

As an example, consider Figure 1, the marked ϵ-NFA for (α?+β?); (β?+γ?);⊤. Intuitively, to travel froms0 to s′ , we need to pass either β or both α and γ. The set of minimal critical sets from s0 to s′ is therefore {{β}, {α, γ}}; if β holds we do not need to test γ to reach s′ . Conversely, the set of maximal critical sets refers to the "worst case" sets of tests to check to travel from s0 to s′ ; here we have {{α, β}, {α, γ}, {β, γ}}. Notice there is no path testing all of α, β, γ, so {α, β, γ} is not a maximal critical set.

We now exploit critical sets to convert an ϵ-NFA for a given dynamic modality to an equivalent alternating automaton. We can achieve this by constructing a suitable transition relation for each state. In particular, we explain how to use the minimal critical sets to construct a transition relation equivalent to that in [Faymonville and Zimmermann, 2015], which was shown to be correct. We show this for the diamond case; the box case is dual. Recall that the transition relations for states of the constructed alternating automaton in [Faymonville and Zimmermann, 2015] for 〈ρ〉φ are defined as follows:

where DRemain = ∨s′∈Sr\{fr} ∨π∈Π(s,s′ ) Pπ, Pπ = ∨t∈Rr (s′ ,A) (t ∧Qm(π) ), QM = ∧θj∈M Rj(s0j ,A) and DLeave = ∨π∈Π(s,fr) (Rφ(s0φ , A) ∧ Qm(π)).

Theorem 1. Let π1 be an ϵ-path from s to s′ in a marked ϵ-NFA A = (Σ, S, s0 , ρ, f,m), for the regular expression ρ. Let M1 be the marking set induced by π1 and suppose M1 is not a minimal critical set. The transition relation for the alternating automaton for 〈ρ〉φ without considering π1 is the same as that considering π1.

Proof. We first show this for DRemain. Consider Pπ1 . Since M1 is not a minimal critical set, by definition there is some minimal critical set M∗ ⊂ M1. We partition M1 into M∗ and Mx = M1 \ M∗. Note that M∗ itself is induced by some ϵ-path π∗ from s to s′ from Definition 6. The inner disjunct of DRemain, ∨π∈Π(s,s′ ) Pπ, includes both Pπ1 and Pπ∗ . Consider that Pπ1 ∨Pπ∗ =

with the second last step holding by the absorption law. Thus, ∨π∈Π(s,s′ ) Pπ = ∨π∈Π(s,s′ )\{π1} Pπ. The proof for DLeave is similar; the other cases for s are independent of Π(s, s′ ).

Given the theorem above, we have DRemain = ∨s′∈Sr\{fr} ∨M∈MinCS(s,s′ ) ∨t∈Rr(s′ ,A) (t ∧ QM), where MinCS(s, s′ ) denotes the set of minimal critical sets from s to s′ . Similarly we have DLeave = ∨M∈MinCS(s,s′ ) (Rφ(s0φ , A) ∧ QM ). For example, for 〈ρ〉φ in Figure 1, we only need to consider the paths π = (1, 3, 4, 5, 6, 8, 9) and π′ = (1, 2, 4, 5, 7, 8, 9) as opposed to all four ϵ-paths between nodes 1 and 9.

Our approach eagerly constructs the alternating automata, and the number of critical sets is potentially superpolynomial. Hence, we may require more than polynomial space. However, this is acceptable for our purposes, as we intend to use this algorithm for symbolic model checking with OBDDs (which themselves already use exponential space). We believe the empirical efficiency that BDDs provide outweighs this disadvantage in practice.

Computing Critical Sets. To compute the set of critical sets between states in an ϵ-NFA we introduce Algorithm 2, which can be seen as a variant of breadth-first search (BFS) over the ϵ-closure of each state in the alternating automaton.

Algorithm 2 Minimal Critical Set Finding Algorithm

INPUT: ϵ-NFAA, state s in A

OUTPUT: MinCS(s, s′ ) for each s′ in the ϵ-closure of s

• 1: Let C be a map of states to sets of sets of tests.
• 2: Let Q be a queue of pairs of states and sets of tests.
• 3: Q.add((s, {}))
• 4: while Q is not empty do
• 5: (s′ , Ts′ ) = Q.dequeue()
• 6: if C[s′ ] = null then C[s′ ] = {Ts′}
• 7: else if ∃x.x ∈ C[s′ ] ∧ x ⊆ Ts′ then
• 8: continue ▷ skip line 12, in particular
• 9: else if ∃x.x ∈ C[s′ ] ∧ Ts′ ⊂ x then
• 10: C[s′ ] = (C[s′ ] ∪ {Ts′ }) \ {x}
• 11: else C[s′ ] = (C[s′ ] ∪ {Ts′ })
• 12: for all ϵ-transitions (s′ , t) do Q.add(t, Ts′ ∪ m(t))
• 13: return C

We maintain C[s′ ], a cache of sets of tests we know we can use to reach the node s′ so far. At each step in the BFS, if C[s′ ] contains a subset of the current test set Ts′ , then we know the current path no longer leads to a (distinct) minimal critical set, so we prune it. The maximal case is analogous. We now show Algorithm 2 returns MinCS(s, s′ ).

Theorem 2. Algorithm 2 returns MinCS(s, s′ ) for each s′ in the ϵ-closure of s.

Proof. (sketch) We first observe that C[s′ ] for any s′ only contains marking sets. This is apparent since only line 12 builds the actual sets, which follows the marking function.

Algorithm 2 cannot skip any minimal critical sets. Firstly, observe that a minimal critical set cannot be removed (line 10), because there is no marking set that is a subset of it. Now suppose that a minimal critical set M was not added. It must be induced by a path π we did not fully traverse (line 7). There must be some node s′′ where it stopped, and some path π′ using fewer tests to get to s′′ . However, the path composed of π′ from s to s′′ and π from s′′ to s′ must use M (as M is minimal). This path must be considered or dropped; if dropped, there must be yet another path using M. Since our ϵ-NFAs are finite, this cannot repeat indefinitely. We must consider some path using M, so M is added, a contradiction.

Furthermore, no other sets are returned - it is apparent that C[s′ ] for any s′ never contains a pair of sets where one is a strict subset of the other, and any other marking set would have as a strict subset some minimal critical set.

Finally, we show our approach is fixed parameter tractable.

Theorem 3. Model checking interpreted systems against LDLK specifications by using Algorithm 1 requires time linear in the size of the model (|G|) and exponential in the size of the formula (|φ|).

Proof. Step 1 requires O(|φ|) recursive runs of Algorithm 1 on formulae known to be smaller. Following ideas from Theorem 6.4 of [Emerson and Lei, 1985], this will not affect the overall complexity (which is clearly superadditive).

Step 2 requires polynomially many runs of Algorithm 2 and building the quantification. The runtime of Algorithm 2 is O(2|φ| log |φ| ) since there are O(2|φ| ) possible sets and it is apparent no set is ever added from the same edge twice. Building the quantification for all states involves iterating over each critical set a linear number of times; again, O(2|φ| log |φ| ).

Step 3 requires time exponential in the size of the alternating automaton [Bloem et al., 2006]. This automaton has size linear in |φ|, so this step is exponential in |φ|.

Step 4 requires time linear in |G| and of the B¨uchi automaton (which is exponential in |φ|) [Burch et al., 1990]. Hence, all steps run in time linear in |G|, and exponential in |φ|.

Note that, while we will show in Section 4 that Algorithm 2 leads to attractive experimental results due to the fact it is amenable to symbolic encoding, it is actually not optimal.

Theorem 4. Model checking interpreted systems against LDLK specifications is PSPACE-complete.

Proof. Hardness follows from PSPACE-completeness of LDL model checking [Faymonville and Zimmermann, 2015]. For membership, the translation above involves model checking polynomially many LDL formulae (requiring polynomial space) and evaluating polynomially many epistemic operators (requiring polynomial space under observational semantics). We can store the labels for polynomially many atomic propositions introduced; again these are of polynomial size.

4 Implementation and Experimental Results

We implemented the algorithms introduced in Section 3 on top of version 1.2.2 of MCMAS [Lomuscio et al., 2015], an open-source BDD-based symbolic model checker. The sources and executables of the resulting toolkit, called MCMASLDLK, are available from [MCMASLDLK, 2017].

For usability reasons, MCMASLDLK supports the standard propositional abbreviations and the box operator. Given an input formula φ, MCMASLDLK first transforms ¬φ to NNF. We then build the alternating automaton, representing states explicitly but transitions symbolically. We associate each state with a BDD variable; this is motivated by the fact that the number of states is polynomial in the formula size. When processing LDL modalities, we explicitly construct ϵNFAs, find critical sets, and convert them to alternating automata, using the construction earlier presented.

MCMAS does not use alternating automata. We thus implemented the symbolic breakpoint construction of [Bloem et al., 2006] to convert our alternating automaton into an equivalent symbolic B¨uchi automaton. We were able to reuse MCMAS's implementation for CTLK with fairness (by checking EG⊤ with suitable fairness constraints), to find states Q for which there exists a path satisfying ¬φ. Following LDLK semantics, Q′ , the complement of Q, constitutes the set of states satisfying φ. We thus check if φ holds in all initial states, by checking if p → q is valid (where p holds in I and q in Q′ ).

In addition to the model checking algorithms, we also implemented counterexample generation. We also inherit fairness constraint support from MCMAS; while LDLK can capture them, we expect native support to be more efficient.

Performance Optimisations. MCMASLDLK employs several optimisations. First, note that the checker's performance is affected by the size of the alternating automata constructed. To mitigate this MCMASLDLK employs:

propositional shortcircuiting (PS): instead of constructing the corresponding alternating automaton, subformulae free of dynamic modalities and states where they hold are identified;

reachability pruning (RP): Since ϵ-NFA states with no inbound non-ϵ transitions are never transitioned to in alternating automata, these are not included in the alternating automata (but are still considered in the ϵ-NFAs to find critical sets).

The automata remain polynomial (so the complexity is unaffected), but we found these optimisations useful in practice.

We further optimised MCMASLDLK for efficiently computing conjuncts (ECC) for the symbolic breakpoint construction, which involves computing TI ∧TLC ∧TR (notation from [Bloem et al., 2006]). We initially computed each term separately, but found it cheaper to first compute a BDD TR, and then use it as an accumulator, taking conjunctions with each term of TI and TLC. We believe this is because our original approach involves conjunctions of large BDDs (which has complexity in the product of BDD sizes [Bryant, 1986]).

Experimental Setup. We report below experiments run on virtual machines with two 2.70GHz CPUs and 16 GB of RAM running Ubuntu v15.10 (Linux kernel v4.2). As a testbed we took the prisoners and lightbulb scenario [Ditmarsch et al., 2010]. We compared MCMASLDLK's performance against MCMAS's for specifications expressible in both CTLK and LDLK, and evaluated the scalability of the approach on suitable LDLK specifications with the number of prisoners N. We report results for both optimised and unoptimised versions of MCMASLDLK.

Comparison with MCMAS. We verified φ0 (CTLK) with MCMAS and φ′0 (LDLK) with MCMASLDLK; it can be checked that the two formulas are equivalent.

In both cases, agent 0 is the counter agent. Both specifications hold for all N, expressing that the counter knows that all prisoners have been interrogated whenever he announces this. The results are reported in Table 1.

Observe that, while the CTLK algorithm performs better than the optimised LDLK algorithm, both algorithms require time on the same order of magnitude. This is in sharp contrast with the underlying complexity of the corresponding decision problems. Further observe that the runtime is dominated by the computations for reachability making the difference in the performance for labelling practically insignificant.

The experiments also show that the optimisations above are essential for the scalability of the tool. In the cases presented PS was particularly significant as the expression within the box modality can be treated as a single atomic proposition.

Scalability assessment. We now report the results obtained when verifying the same scenario against the property

φ1 holds iff on all paths the lightbulb is not repeatedly toggled until the counter knows the prisoners are released. In the scenario we can realise such a path by alternating the selection of a fresh non-counter with the counter; so φ1 is false for any N. The results obtained are in Table 2.

As before, we observe that the LDLK algorithm appears able to scale reasonably well with the size of the model (for N = 50, we have 2.19×1025 reachable states). The optimisations implemented provide a small performance improvement (largely due to RP and ECC). The case N = 40 is an exception, probably owing to optimisation overheads that in this case perform poorly. Further experiments, not here discussed but included in the software package [MCMASLDLK, 2017], demonstrate that MCMASLDLK scales well with large models but not so with long formulae. This is to be expected given Theorem 3 and, for similar reasons, it is also a feature of LTL model checkers. This is not normally considered to be too problematic since specifications are typically rather short.

5 Conclusions

As stated in the Introduction, LDL has recently been put forward as a powerful specification language for distributed systems and AI systems. A key attractiveness of LDL is that while it has the same expressivity as ω-regular languages, the complexity of the associated model checking problem is the same as LTL.

In this paper we have augmented LDL with epistemic operators and provided a semantics of the logic in terms of interpreted systems. The key contribution of the paper rests in the formulation of a model checking procedure for LDLK that is amenable to symbolic implementation. In fact, while the complexity of the model checking problem for LDL is known, no symbolic procedure, nor implementation is available. The resulting algorithm, based on the notion of critical sets for ϵ-NFA, was implemented as MCMASLDLK, an extension of the open-source model checker MCMAS. Our testing and the experimental results showed that MCMASLDLK correctly supports LDLK, offers attractive performance and has little overhead on the fragments of LDLK also expressible in CTLK (already supported by MCMAS). To achieve efficiency, particular effort was devoted to several optimisations to handle the automata and OBDDs during verification.

In future work we intend to extend the results here presented to support finite traces, which is the object of recent work in the area [De Giacomo and Vardi, 2015].