SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems (Extended Abstract) ? Bożena Woźna-Szcześniak IMCS, Jan Długosz University. Al. Armii Krajowej 13/15, 42-200 Czȩstochowa, Poland. b.wozna@ajd.czest.pl Abstract. We present WECTL∗ KD, a weighted branching time temporal logic to specify knowledge, and correct functioning behaviour in multi-agent systems (MAS). We interpret the formulae of the logic over models generated by weighted deontic interpreted systems (WDIS). Furthermore, we investigate a SAT-based bounded model checking (BMC) technique for WDIS and for WECTL∗ KD. 1 Introduction The formalism of interpreted systems (IS) [4] provides a useful framework to model multi-agent systems (MASs) [13], and to verify various classes of temporal and epis- temic properties. The formalism of deontic interpreted systems (DIS) [7] is an extension of ISs, which makes possible reasoning about temporal, epistemic and correct function- ing behaviour of MASs. An important assumption in this line of models is that there are no costs associated to agents’ actions. The formalism of weighted deontic interpreted systems (WDISs) [16] extends DISs to make the reasoning possible about not only tem- poral, epistemic and deontic properties, but also about agents quantitative properties. In particular, in the Kripke model of WDIS each transition is labelled by a pair: a joint action and a positive integer value that represents the cost of acting agents. The basic idea in SAT-based bounded model checking (BMC) [1, 9] is to translate the existential model checking problem for a modal (e.g., temporal, epistemic, deontic) logic [2, 13] to the propositional satisfiability problem. In particular, in BMC we first represent a counterexample, whose length is bounded by some integer k, by a propo- sitional formula, and then check the resulting propositional formula with a specialised SAT-solver. If the formula in question is satisfiable, then the SAT-solver returns a satis- fying assignment that can be converted into a concrete counterexample. Otherwise, the bound k is increased and the process repeated; we increases k until either a witness is found, the problem becomes intractable, or some pre-known upper bound is reached. To model check the requirements of MASs various extensions of temporal logics [3] with epistemic [4], beliefs [6], and deontic [7] components have been proposed. In this paper we aim at completing the picture of applying the SAT-based BMC techniques to MASs by looking at the existential fragment of the weighted CTL∗ KD (i.e. weighted CTL∗ extended with epistemic and deontic components), interpreted over the weighted deontic interpreted systems (WDISs). The proposed BMC encoding is based on the ? Partly supported by National Science Center under the grant No. 2011/01/B/ST6/05317. BMC encoding introduced in [16, 21, 24]. Namely, in [24] a propositional encoding of the BMC problem for ECTL∗ and for standard Kripke models has been introduced. The method has been experimentally evaluated. Next, in [16] weighted deontic interpreted systems (WDIS) and a propositional encoding of the BMC problem for WECTLKD and for WDIS have been introduced. Finally, in [21] a BMC method for WELTLK and for weighted interpreted systems has been introduced and experimentally evaluated. The rest of the paper is organised as follows. In Section 2 we introduce WDIS together with its Kripke model. In Section 3 we define the WECTL∗ KD language to- gether with the bounded semantics. In Section 4 we provide a SAT-based BMC method for WECTL∗ KD and for WDIS. In the last section we conclude the paper. Fig. 1. Classical temporal and weighted logics with discrete semantics, and their epistemic and deontic extensions. The dedicated SAT-based BMC methods have been defined for the logics placed in rectangles. The logics for which SAT-BMC methods can be easily inferred from the dedicated one are placed in ”dashed” rectangles. Related work. Figure 1 provides diagram showing the relations between classical tem- poral logics, weighted temporal logics, and their epistemic and deontic extensions, and indicates for which logic a SAT-based BMC method (SAT-BMC for short) has been developed. For classical temporal logics with discrete semantics over Kripke mod- els SAT-BMC has been defined in [1] for LTL, in [10, 23] for ECTL, in [14, 24] for ECTL? , in [22] for RTECTL, and in [12] for MTL. For classical weighted tempo- ral logics with discrete semantics over weighted Kripke models generated, for exam- ple, by simply timed systems, SAT-BMC has been defined for WECTL [20] only. For epistemic and deontic variants of classical temporal logics with semantics over Kripke models generated by (deontic) interpreted systems SAT-BMC has been defined in [9, 5] for ECTLK, in [15] for ECTLKD, in [11, 8] for ELTLK, in [19] for RTECTLK, in [18] for RTECTLKD, and in [17] for EMTLKD (this method provides obviously a SAT-BMC solution for EMTLK). There is no paper about SAT-BMC for ECTL? K and for ECTL? KD. These missing methods can however be easily designed as a fu- sion of SAT-BMC methods for ECTL? and for ECTLK / ECTLKD. For epistemic and deontic variants of classical weighted temporal logic with semantics over Kripke models generated by (deontic) weighted interpreted systems SAT-BMC has been de- fined in [21] for WELTLK (this method provides obviously a SAT-BMC solution for WELTL), and in [16] for WECTLKD (this method provides obviously a SAT-BMC solution for WECTLK). 2 Weighted Deontic Interpreted Systems Let Ag = {1, . . . , n} be the non-empty and finite set of agents. We assume that a MAS consists of n agents and a special agent E that represent the environment in which the agents operate. Next, we assume that a given MAS is modelled by the weighted deontic interpreted system (WDIS), in which each agent c ∈ Ag ∪ {E} is modelled using a non-empty set Lc = Gc ∪ Rc of local states such that Gc is a non-empty set of faultless (green) states and Rc is a set of faulty (red) states, a non-empty set ιc ⊆ Lc of initial states, a non-empty set Actc of possible actions, a protocol function Pc : Lc → 2Actc that defines rules according to agents operate, a (partial) evolution function tc : Lc × Act → Lc with Act = Act1 × · · · × Actn × ActE (each element of Act is called a joint action), a weight function dc : Actc → IN, and a valuation function Vc : Lc → 2PV that assigns to each local state a set of propositional variables that are assumed to be true at that state. Further, we do not assume that the sets Actc are disjoint for all c ∈ Ag ∪ {E}. Now for a given set of agents Ag, the environment E and a set of propositional variables PV, we define the weighted deontic interpreted system as a tuple WDIS = ({ιc , Lc , Gc , Actc , Pc , tc , Vc , dc , }c∈Ag∪{E} ). For a given WDIS we define: • a set of all possible global states S = L1 × . . . × Ln × LE such that L1 ⊇ G1 , . . . , Ln ⊇ Gn , LE ⊇ GE ; by lc (s) we denote the local component of agent c ∈ Ag ∪ {E} in a global state s = (`1 , . . . , `n , `E ); a • a global evolution function t : S × Act → S as follows: t(s, a) = s0 (or s −→ s0 ) iff for all c ∈ Ag, tc (lc (s), a) = lc (s0 ) and tE (lE (s), a) = lE (s0 ); • a weighted model (or a model) as a tuple M = (ι, S, T, V, d), where • ι = ι1 × . . . × ιn × ιE is the set of all possible initial global state; • S is the set of all possible global states as defined above; • T ⊆ S×Act×S is a transition relation defined by the global evolution function a as follows: (s, a, s0 ) ∈ T iff s −→ s0 . We assume that the relation T is total, i.e., for any s ∈ S there exists s0 ∈ S and an action a ∈ Act\{(1 , . . . , n , E )} a such that s −→ s0 ; PV S • V : S → 2 is the valuation function defined as V(s) = c∈Ag∪{E} Vc (lc (s)). • d : Act → P IN is a “joint” weight function defined as follows: d((a1 , . . . , an , aE )) = c∈Ag∪{E} dc (ac ); note that this definition is reasonable, since we are interested in MASs, in which transitions carry some cost; • an indistinguishability relation ∼c ⊆ S × S for agent c as follows: s ∼c s0 iff lc (s0 ) = lc (s); • a deontic relation ∝c ⊆ S × S for agent c as follows: s ∝c s0 iff lc (s0 ) ∈ Gc . 1 a 2 a 3 a A path in M is an infinite sequence π = s0 −→ s1 −→ s2 −→ . . . of transitions. For such a path, and for j 6 m ∈ IN, by π(m) we denote the m-th state sm , by π m we denote the m-th suffix of the path π, which is defined in the standard way: am+1 am+2 π m = sm −→ sm+1 −→ sm+2 . . .. Next, by π[j..m] we denote the finite sequence aj+1 aj+2 sj −→ sj+1 −→ . . . sm with m − j transitions and m − j + 1 states, and by Dπ[j..m] we denote the (cumulative) weight of π[j..m] that is defined as d(aj+1 ) + . . . + d(am ) (hence 0 whenS j = m). By Π(s) we denote the set of all the paths starting at s ∈ S, and by Π = s0 ∈ι Π(s0 ) we denote the set of all the paths starting at initial states. 3 The logic WECTL∗ KD Our specification language, which we call WECTL∗ KD, extends ECTL∗ [3] with cost constraints on temporal modalities and with epistemic and deontic modalities. More precisely, the basic modalities of WECTL∗ KD consist of the path quantifier E (for some path) followed by a temporal-epistemic-deontic formula, which is built up from: propo- sitional variables; the boolean operators (∧-conjunction, ∨-disjunction, ¬-negation); the temporal modalities (XI -weighted next step, UI -weighted until, RI -weighted re- lease, GI -weighted always, and FI -weighted sometime); the epistemic modalities Kc (for “agent c does not know whether or not”), DΓ , EΓ , and CΓ (for the dualities to the standard group epistemic modalities representing distributed knowledge in the group Γ , everyone in Γ knows, and common knowledge among agents in Γ ); the deontic modal- ities (Oc and Kb c2 representing the correctly functioning circumstances of agents). c1 Syntax of WECTL∗ KD. Let p ∈ PV be a propositional variable, c, c1 , c2 ∈ Ag, Γ ⊆ Ag, and I be an interval in IN = {0, 1, 2, . . .} of the form: [a, b) and [a, ∞), for a, b ∈ IN and a 6= b. We have the following syntax for WECTL∗ KD. We inductively define a class of state formulae (interpreted at states) and a class of path formulae (interpreted along paths) by the following grammar: b c2 φ ϕ ::=true | false | p | ¬p | ϕ ∧ ϕ | ϕ ∨ ϕ | Eφ | Kc φ | EΓ φ | DΓ φ | CΓ φ | Oc φ | K c1 φ ::=ϕ | φ ∧ φ | φ ∨ φ | XI φ | φUI φ | φRI φ where ϕ is a state formula and φ is a path formula. WECTL∗ KD consists of the set of state formulae generated by the above grammar. The derived basic temporal path modalities for weighted eventually (FI ) and weighted globally (GI ) are defined as follows: FI φ ::= trueUI φ, and GI φ ::= falseRI φ. Note that the combination of weighted temporal, epistemic and deontic operators allows us to specify how agent’s knowledge or correctly functioning circumstances of agents evolve over time and how much they cost. Semantics of WECTL∗ KD. The semantics of WECTL∗ KD formulae is determined with respect to a model, defined in Section 2. In the semantics we assume the follow- def S C def ing definitions of epistemic relations: ∼EΓ = E + c∈Γ ∼c , ∼Γ = (∼Γ ) (the transitive D def closure of ∼E T Γ ), ∼Γ = c∈Γ ∼c , where Γ ⊆ Ag. Definition 1. Let M be a model, s a state of M , π a path in M , and m ∈ IN. For a state formula α over PV, the notation M, s |= α means that α holds at the state s in the model M . Similarly, for a path formula ϕ over PV, the notation M, π |= ϕ means that ϕ holds along the path π in the model M . Moreover, let p ∈ PV be a propositional variable, α, β be state formulae of WECTL∗ KD, and ϕ, ψ be path formulae of WECTL∗ KD. The relation |= is defined inductively as follows: M, s |= true, M, s 6|= false, M, s |= p iff p ∈ V(s), M, s |= ¬p iff p ∈ / V(s), M, s |= α ∧ β iff M, s |= α and M, s |= β, M, s |= α ∨ β iff M, s |= α or M, s |= β, M, s |= Kc α iff (∃π ∈ Π)(∃i > 0)(s ∼c π(i) and M, π i |= α), M, s |= Y Γ α iff (∃π ∈ Π)(∃i > 0)(s ∼YΓ π(i) and M, π i |= α), Y ∈ {D, E, C}, M, s |= Oc α iff (∃π ∈ Π)(∃i > 0)(s ∝c π(i) and M, π i |= α), c2 M, s |= K b α c1 iff (∃π ∈ Π)(∃i > 0)(s ∼c1 π(i) and s ∝c2 π(i) and M, π i |= α), M, s |= Eϕ iff (∃π ∈ Π(s))(M, π 0 |= ϕ), m M, π |= α iff M, π(m) |= α, M, π m |= ϕ ∧ ψ iff M, π m |= ϕ and M, π m |= ψ, M, π m |= ϕ ∨ ψ iff M, π m |= ϕ or M, π m |= ψ, M, π m |= XI ϕ iff Dπ[m..m + 1] ∈ I and M, π m+1 |= ϕ, M, π m |= ϕUI ψ iff (∃j > m) Dπ[m..j] ∈ I and M, π j |= ψ and (∀m 6 i < j)M, π i |= ϕ , m M, π |= ϕRI ψ iff (∃j > m) Dπ[m..j]  ∈ I and M, π j |= ϕ and (∀m 6 i 6 j) M, π i |= ψ or (∀j > m)(Dπ[m..j] ∈ I implies M, π j |= ψ). A WECTL∗ KD state formula α is true in the model M , denoted by M |= α, iff for some s ∈ ι, M, s |= α, i.e., α holds at some initial state of M . The model checking problem asks whether M |= α. Bounded semantics of WECTL∗ KD. A bounded semantics for WECTL∗ KD is the ba- sis of the translation of bounded model checking problem to the satisfiability of propo- sitional formulae problem (i.e., SAT-problem) that is defined in the next section. To define the bounded semantics we need to represent infinite paths of a model in a special way. To this aim, as usually, we define the notions of k-paths and loops. Definition 2. Let M be a model, k ∈ IN a bound, and 0 6 l 6 k. A k-path πl is a pair a1 a2 ak (π, l), where π is a finite sequence s0 −→ s1 −→ . . . −→ sk of transitions. A k-path πl is a loop if l < k and π(k) = π(l). Note that if a k-path πl is a loop, then it represents the infinite path of the form uv ω , a1 a2 al al+2 ak where u = (s0 −→ s1 −→ . . . −→ sl ) and v = (sl+1 −→ S . . . −→ s0k ). Πk (s) denotes the set of all the k-paths of M that start at s, and Πk = s0 ∈ι Πk (s ). As in the definition of bounded semantics we need to define the satisfiability relation on suffixes of k-paths, we denote by πlm the pair (πl , m), i.e. the k-path πl together with the designated starting point m, where 0 6 m 6 k. Further, let s be a state and πl be a k-path. For a state formula α over PV, the notation M, s |=k α means that α is k-true at the state s in the model M . Similarly, for a path formula ϕ over PV, the notation M, πlm |=k ϕ, where 0 6 m 6 k, denotes that the formula ϕ is k-true along the suffix am+1 am+2 ak π(m) −→ π(m + 1) −→ . . . −→ π(k) of π. Definition 3. Let M be a model, s a state of M , πl a k-path in M , 0 6 m 6 k, p ∈ PV a propositional variables, α, β state formulae of WECTL∗ KD, and ϕ, ψ path formulae of WECTL∗ KD. The relation |=k is defined inductively as follows: M, s |=k true, M, s 6|=k false, M, s |=k p iff p ∈ V(s), M, s |=k ¬p iff p ∈ / V(s), M, s |=k α ∧ β iff M, s |=k α and M, s |=k β, M, s |=k α ∨ β iff M, s |=k α or M, s |=k β, M, s |=k Kc α iff (∃πl ∈ Πk )(∃0 6 j 6 k)(M, πlj |=k α and s ∼c π(j)), M, s |=k Y Γ α iff (∃πl ∈ Πk )(∃0 6 j 6 k)(M, πlj |=k α and s ∼YΓ π(j)), where Y ∈ {D, E, C}, M, s |=k Oc α iff (∃πl ∈ Πk )(∃0 6 j 6 k)(M, πlj |=k α and s ∝c π(j)), M, s |=k Kb c2 α iff (∃πl ∈ Πk )(∃0 6 j 6 k)(M, πlj |=k α and s ∼c1 π(j) c1 and s ∝c1 π(j)), M, s |=k Eϕ iff (∃πl ∈ Πk (s))(M, πl0 |=k ϕ), M, πlm |=k α iff M, π(m) |=k α, M, πlm |=k ϕ ∧ ψ iff M, πlm |=k ϕ and M, πlm |=k ψ, M, πlm |=k ϕ ∨ ψ iff M, πlm |=k ϕ or M, πlm |=k ψ, M, πlm |=k XI ϕ iff (m < k and Dπ[m..m + 1] ∈ I and M, πlm+1 |=k ϕ) or (m = k and l < k and π(k) = π(l) and Dπ[l..l + 1] ∈ I and M, πll+1 |=k ϕ), M, πl |=k ϕUI ψ iff (∃m 6 j 6 k)(Dπ[m..j] ∈ I and M, πlj |=k ψ and m (∀m 6 i < j)M, πli |=k ϕ)or(l < m and π(k) = π(l) and (∃l < j < m)(Dπ[m..k] + Dπ[l..j] ∈ I and M, πlj |=k ψ and (∀l < i < j)M, πli |= ϕ and (∀m 6 i 6 k)M, πli |=k ϕ)), m M, πl |=k ϕRI ψ iff (Dπ[m..k] > right(I) and (∀m 6 j 6 k)(Dπ[m..j] ∈ I implies M, πlj |=k ψ)) or (Dπ[m..k] < right(I) and π(k) = π(l) and (∀m 6 j 6 k)(Dπ[m..j] ∈ I implies M, πlj |=k ψ) and (∀l 6 j 6 k)(Dπ[m..k] + Dπ[l..j] ∈ I implies M, πlj |=k ψ)) or (∃m 6 j 6 k)(Dπ[m..j] ∈ I and M, πlj |=k ϕ and (∀m 6 i 6 j)M, πli |=k ψ) or (l < m and π(k) = π(l) and (∃l < j < m)(Dπ[m..k] + Dπ[l..j] ∈ I and M, πlj |=k ϕ and (∀l < i 6 j)M, πli |= ψ and (∀m 6 i 6 k)M, πli |=k ψ)). A WECTL∗ KD state formula α is k-true in M , denoted M |=k ϕ, iff for some s ∈ ι, M, s |=k ϕ. The bounded model checking problem asks whether there exists k ∈ IN such that M |=k ϕ. Lemma 1. Let M be a model, s a state of M , and α a WECTL∗ KD state formula. • for some k ∈ IN, if M, s |=k α, then M, s |= α. • if M, s |= α, then M, s |=k α for some k ∈ IN. The following theorem follows from Lemma 1 and it states that for a given model M and a formula α there exists a bound k such that the model checking problem can be reduced to the bounded model checking problem. Theorem 1. Let M be a model and α be a WECTL∗ KD state formula. Then, for some s ∈ ι, M, s |= α iff M, s |=k α for some k ∈ IN. 4 Bounded Model Checking In the section we present a propositional encoding of the bounded model checking problem for WECTL∗ KD and for weighted deontic interpreted systems (WDIS). Let M = (ι, S, T, V, d) be a model, α a WECTL∗ KD state formula, and k > 0 a bound. The BMC encoding relies on defining the following propositional formula: [M, α]k := [M α,ι ]k ∧ [α]M,k , which is satisfiable if and only if M |=k α holds. The definition of [M α,ι ]k assumes that the states, the joint actions of M , and the sequence of weights associated to the joint actions are encoded symbolically, which is possible, since both the set of states and the set of joint actions are finite. Formally, let c ∈ Ag ∪ {E}. Then, each state s = (`1 , . . . , `n , `E ) ∈ S is represented by a symbolic state which is a vector w = (w1 , . . . , wn , wE ) of symbolic local states. Each symbolic local state wc is a vector of propositional variables (called state variables) whose length depends on the number of green and red local states of agent c. Next, each joint action a = (a1 , . . . , an , aE ) ∈ Act is represented by a symbolic action which is a vector a = (a1 , . . . , an , aE ) of symbolic local actions. Each symbolic local action ac is a vector of propositional variables (called action variables) whose length depends on the number of actions of agent c. Next, each vector of weights associated to a joint action is represented by a symbolic weight which is a vector d = (d1 , . . . , dn , dE ) of symbolic local weights. Each symbolic local weight dc is a vector of propositional variables (called weight variables), whose length depends on the weight functions dc . Further, we assume that SV , AV and W V denote, respectively, the set of all the state variables, the set of all the action variables, and the set of all the weight variables such that SV ∩ AV = ∅, SV ∩ W V = ∅, and AV ∩ W V = ∅. Next, we assume that SV (w), SV (wc ), AV (a), AV (ac ), and W V (d) denote, respectively, the set of all the state variables occurring in the symbolic state w, the set of all the state variables occurring in the local symbolic state wc of agent c, the set of all the action variables occurring in the symbolic action a, the set of all the action variables occurring in the local symbolic action ac of agent c, and the set of all the weight variables occurring in the symbolic weight d. Furthermore, we assume that N V denotes the set of proposi- tional variables (called the natural variables) such that SV ∩ N V = ∅, AV ∩ N V = ∅, and W V ∩ N V = ∅. Moreover, by u = (u1 , . . . , uy ) we denote a vector of natural variables of length y = max(1, dlog2 (k + 1)e), which we call a symbolic number, and by N V (u) we denote the set of all the natural variables occurring in u. Furthermore, we assume that: • P V = SV ∪ AV ∪ W V ∪ N V . • lit : {0, 1} × P V → P V ∪ {¬q | q ∈ P V } is a function defined as: lit(1, q) = q and lit(0, q) = ¬q. • V : P V → {0, 1} is a valuation of propositional variables (a valuation for short). • rw denotes the length of symbolic state, i.e. w = (w1 , . . . , wn , wE ) = (w1 , . . . , wrw ). • ra denotes the length of a symbolic action, i.e. a = (a1 , . . . , an , aE ) = (a1 , . . . , ara ), • rd = rd1 + . . . + rd(n+1) denotes the length of a symbolic weight, i.e. d = (d1 , . . . , dn , dE ) = (d11 , . . . , d1rd1 , . . . , dn+1 1 , . . . , dn+1 rd(n+1) ), where rd1 , . . . , rd(n+1) denote lengths of local symbolic weights. For every rw , ra , rd ∈ IN+ , each valuation V induces the functions S : SV rw → {0, 1}rw , A : AV ra → {0, 1}ra , W : W V rd → IN, and J : N V y → IN defined in the following way: S((w1 , . . . , wrw )) = (V (w1 ), . . . , V (wrw )), A((a1 , . . . , ara )) = Pn+1 Prdj j (V (a1 ), . . . , V (ara )), W((d11 , . . . , d1rd1 , . . . , dn+1 1 , . . . , dn+1 rd(n+1) )) = j=1 i=1 V (di )· y 2i−1 , J((u1 , . . . , uy )) = i=1 V (ui ) · 2i−1 . P Let w and w0 be two different symbolic states such that SV (w) ∩ SV (w0 ) = ∅, d a symbolic weight, a a symbolic action, and u a symbolic number. We assume definitions of the following auxiliary Boolean formulae: • p(w) is a Boolean formula over SV (w) that is true for a valuation V iff p ∈ V(S(w)). V It encodes a set of states of M in which p ∈ PV holds. rw • Is (w) = i=1 lit(s[i], wi ). This Boolean formula is defined over SV (w), and it encodes the state Vrsw of the model M. • H(w, w0 ) = i=1 wi ⇔ w0 i . This Boolean formula is defined over SV (w) ∪ SV (w0 ), and it encodes equality of two symbolic states, i.e. it expresses that the symbolic states w and w0 represent the same states. • Hc (w, w0 ) is a Boolean formula over SV (w) ∪ SV (w0 ) that is true for each valua- tion V ∈ {0, 1}SV such that V satisfies Hc (w, w0 ) iff S(w) ∼c S(w0 ); it expresses that the local states of agent c are the same in the symbolic states w and w0 . • Ha (ac ) for c ∈ Ag ∪ {E} and a ∈ Actc ∪ {ε} is a Boolean formula over AV (ac ) that is true for each valuation V ∈ {0, 1}AV such that V satisfies Ha (ac ) iff A(ac ) = a.V V V • A(a) = a∈Act ( c∈Ag(a) Ha (ac ) ∨ c∈Ag(a) Hε (ac )), where Ag(a) = {c ∈ Ag ∪ {E} | a ∈ Actc }. This formula is defined over AV (a), and it encodes that each symbolic local action ac of a has to be executed by each agent in which it appears. • Tc (wc , (a, d), w0 c ) is defined over SV (wc ) ∪ SV (w0 c ), and is true for a valuation V iff tc (S(wc ), A(a)) = S(w0 c ). This Boolean formula encodes the local evolution function of agent c. V • T (w, (a, d), w0 ) = c∈Ag∪{E} Tc (wc , (a, d), w0c ) ∧ A(a). This Boolean formula is defined over SV (w) ∪ SV (w0 ) ∪ AV (a) ∪ W V (d), and it encodes the transition relation of the model M . • Nj∼ (u) is a formula over N V (u) that is true for a valuation V iff j ∼ J(u), where ∼∈ {<, >, 6, =, >}. This formula encodes that the value j is in the arithmetic relation ∼ with the value represented by the symbolic number u. Further, in order to define [M α,ι ]k we need to specify the number of k-paths of the model M that are sufficient to validate α. Let p ∈ PV. To calculate the number, we de- fine the following auxiliary function fk : WECTL∗ KD → IN: fk (true) = fk (false) = 0, fk (p) = fk (¬p) = 0, fk (ϕ∧φ) = fk (ϕ)+fk (φ), fk (ϕ∨φ) = max{fk (ϕ), fk (φ)}, fk (XI ϕ) = fk (ϕ), fk (ϕUI φ) = k·fk (ϕ)+fk (φ), fk (ϕRI φ) = (k+1)·fk (φ)+fk (ϕ), fk (CΓ ϕ) = fk (ϕ) + k, fk (Y ϕ) = fk (ϕ) + 1, for Y ∈ {Kc , DΓ , EΓ , Oc , Kb c2 , E}. c1 Furthermore, we define the j-th symbolic k-path π j as the sequence of symbolic a1,j ,d1,j a2,j ,d2,j ak,j ,dk,j transitions: (w0,j −→ w1,j −→ . . . −→ wk,j , u), where wi,j are symbolic states, ai,j are symbolic actions, di,j are symbolic weights, for 0 6 i 6 k and 1 6 j 6 fk (α), and u is the symbolic number, and we define the following auxiliary Boolean formulae. Let w and w0 be two different symbolic states, d a symbolic weighs, a a symbolic action, u a symbolic number, I an interval in IN of the form: [a, b) and [a, ∞), for a, b ∈ IN and a 6= b, and right(I) denote the right end of the interval I. • Llk (π n ) := Nl= (un ) ∧ H(wk,n , wl,n ). Sk • BkI (π n ) is defined over i=1 W V (di,n ), and is true for a valuation V iff Pk i=1 W(di,n ) 6 right(I). This Boolean formula encodes that the weight rep- resented by the sequence d1,n , . . . , dk,n is less than or equal to right(I). I • Da,b (π n ) for a 6 b: if a < b, then the formula encodes that the weight represented by the sequence da+1,n , . . . , db,n belongs to the interval I, i.e. the formula is true Pb I for a valuation V iff i=a+1 W(di,n ) ∈ I; otherwise, i.e. if a = b, then Da,b (π n ) is true for a valuation V iff 0 ∈ I. I • Da,b;c,d (π n ) for a 6 b and c 6 d: 1. if a < b and c < d, then the formula encodes that the weight represented by the sequences da+1,n , . . . , db,n and dc+1,n , . . . , dd,n belongs to the interval I, i.e. Pb Pd the formula is true for a valuation V iff i=a+1 W(di,n )+ i=c+1 W(di,n ) ∈ I; 2. if a = b and c < d, then the formula encodes that the weight represented by the sequence dc+1,n , . . . , dd,n belongs to the interval I, i.e. the formula is true Pd for a valuation V iff i=c+1 W(di,n ) ∈ I; 3. if a < b and c = d, then the formula encodes that the weight represented by the sequence da+1,n , . . . , db,n belongs to the interval I, i.e. the formula is true Pb for a valuation V iff i=a+1 W(di,n ) ∈ I; I 4. if a = b and c = d, then Da,b;c,d (π n ) is true for a valuation V iff 0 ∈ I. α,ι The formula [M ]k , which encodes the unfolding of the transition relation of the model M fk (α)-times to the depth k, is defined as follows: fk (α) k fk (α) k−1 _ ^ _ ^ ^ α,ι [M ]k := Is (w0,0 ) ∧ Nl= (uj ) ∧ T (wi,j , (ai,j , di,j ), wi+1,j ) s∈ι j=1 l=0 j=1 i=0 where wi,j , ai,j , di,j , and uj are, respectively, symbolic states, symbolic actions, sym- bolic weights, and symbolic numbers, for 0 6 i 6 k and 1 6 j 6 fk (α). Then, the next step is a translation of a WECTL∗ KD state formula α to a proposi- tional formula [α]M,k . In order to define [α]M,k , we have to know how to divide the set A of k-paths such that |A| = fk (α) into subsets needed for translating the subformu- lae of α. To accomplish this goal we use some auxiliary functions that were defined in [24]. We recall their definitions now. First, the relation ≺ is defined on the power set of IN as follows: A ≺ B iff for all natural numbers x and y, if x ∈ A and y ∈ B, then x < y. Further, let A ⊂ IN be a finite non-empty set, and n, m ∈ IN, where m 6 |A|. Then, gl (A, m) denotes the subset B of A such that |B| = m and B ≺ A \ B, gr (A, m) denotes the subset C of A such that |C| = m and A \ C ≺ C, gs (A) denotes the set A \ {min(A)}, and if n divides |A| −S m, then hp(A, m, n) denotes the se- n quence (B0 , . . . , Bn ) of subsets of A such that j=0 Bj = A, |B0 | = . . . = |Bn−1 |, |Bn | = m, and Bi ≺ Bj for every 0 6 i < j 6 n. Now let hU k (A, m) := hp(A, m, k) and hR k (A, m) := hp(A, m, k +1). Note that if h U k (A, m) = (B 0 , . . . , Bk ), then hU k (A, m)(j) denotes the set B j , for every 0 6 j 6 k. Similarly, if hR k (A, m) = (B0 , . . . , Bk+1 ), then hRk (A, m)(j) denotes the set B j , for every 0 6 j 6 k + 1. The functions gl and gr are used in the translation of the formulae with the main connective being either conjunction or disjunction: for a given WECTL∗ KD formula ϕ ∧ ψ, if the set A is used to translate this formula, then the set gl (A, fk (ϕ)) is used to translate the subformula ϕ and the set gr (A, fk (ψ)) is used to translate the subformula ψ; for a given WECTL∗ KD formula ϕ ∨ ψ, if the set A is used to translate this formula, then the set gl (A, fk (ϕ)) is used to translate the subformula ϕ and the set gl (A, fk (ψ)) is used to translate the subformula ψ. The function gs is used in the translation of the formulae with the main connective Q ∈ {E, Kc , DΓ , EΓ , Oc , K b c2 }: for a given WECTL∗ KD formula Qϕ, if the set A is c1 used to translate this formula, then the path of the number min(A) is used to translate the operator Q and the set gs (A) is used to translate the subformula ϕ. The function hU k is used in the translation of subformulae of the form ϕUI ψ: if the set A is used to translate the subformula ϕUI ψ at the symbolic k-path π n (with the starting point m), then for every j such that m 6 j 6 k, the set hU k (A, fk (ψ))(k) is used to translate the formula ψ along the symbolic path π n with starting point j; moreover, for every i such that m 6 i < j, the set hU k (A, fk (ψ))(i) is used to translate the formula ϕ along the symbolic path π n with starting point i. Notice that if k does not divide |A| − d, then hU k (A, d) is undefined. However, for every set A such that |A| = fk (ϕUI ψ), it is clear from the definition of fk that k divides |A| − fk (ψ). The function hR k is used in the translation of subformulae of the form ϕRI ψ: if the set A is used to translate the subformula ϕRI ψ along a symbolic k-path π n (with the starting point m), then for every j such that m 6 j 6 k, the set hR k (A, fk (ϕ))(k+1) is used to translate the formula ϕ along the symbolic paths π n with starting point j; moreover, for every i such that m 6 i 6 j, the set hR k (A, fk (ϕ))(i) is used to translate the formula ψ along the symbolic path π n with starting point i. Notice that if k + 1 does not divide |A| − 1, then hR k (A, p) is undefined. However, for every set A such that |A| = fk (ϕRI ψ), it is clear from the definition of fk that k + 1 divides |A| − fk (ϕ). Let α be a WECTL∗ KD state formula and A ⊂ IN+ be a set of numbers of symbolic [m,n,A] k-paths such that |A| = fk (α). If n ∈ IN \ A and 0 6 m 6 k, then by hαik we ∗ denote the translation of a WECTL KD state formula α at the symbolic state wm,n by using the set A. Let ϕ be a WECTL∗ KD path formula and B ⊂ IN+ be a set of numbers of symbolic k-paths such that |B| = fk (ϕ). If n ∈ IN+ \ A and 0 6 m 6 k, [m,n,A] then by [ϕ]k we denote the translation of a WECTL∗ KD path formula ϕ along the symbolic k-path π n with starting point m by using the set A. Furthermore, we define [0,0,Fk (α)] [α]M,k as hαik , where Fk (α) = {j ∈ IN | 1 6 j 6 fk (α)}, and: [m,n,A] [m,n,A] htrueik := true, hfalseik := false, [m,n,A] [m,n,A] hpik := p(wm,n ), h¬pik := ¬p(wm,n ), [m,n,A] [m,n,gl (A,fk (α))] [m,n,gr (A,fk (β))] hα ∧ βik := hαik ∧ hβik , [m,n,A] [m,n,gl (A,fk (α))] [m,n,gr (A,fk (β))] hα ∨ βik := hαik ∨ hβik , [m,n,A] [0,min(A),gs (A)] hEϕik := H(wm,n , w0,min(A) ) ∧ [ϕ]k , [m,n,A] [m,n,A] [α]k := hαik , [m,n,A] [m,n,gl (A,fk (ϕ))] [m,n,gr (A,fk (ψ))] [ϕ ∧ ψ]k := [ϕ]k ∧ [ψ]k , [m,n,A] [m,n,gl (A,fk (ϕ))] [m,n,gr (A,fk (ψ))] [ϕ ∨ ψ]k := [ϕ]k ∨ [ψ]k , ( [m+1,n,A] [m,n,A] DI (π n ) ∧ [α]k , if m < k [XI α]k := Wm,m+1k−1 I l [l+1,n,A] l=0 (Dl,l+1 (π n ) ∧ Lk (π n ) ∧ [α]k ), if m = k [m,n,A] Wk I [j,n,hU k (k)] Vj−1 [i,n,hUk (i)] [αUI β]k := j=m (Dm,j (π n ) ∧ [β]k ∧ i=m [α]k )∨ Wm−1 l Wm−1 > [j,n,hU k (k)] ( l=0 Lk (π n )) ∧ j=0 (Nj (un ) ∧ [β]k ∧ Wm−1 = I l=0 (N l (u n ) ∧ D m,k;l,j (π n ))∧ Vj−1 > [i,n,hU k (i)]  Vk [i,n,hU k (i)] i=0 (N i (u n ) → [α] k ) ∧ i=m [α]k ), R R [m,n,A] Wk I [j,n,hk (k)] V j [i,n,hk (i)] [αRI β]k := j=m (Dm,j (π n ) ∧ [α]k ∧ i=m [β]k )∨ Wm−1 l Wm−1 > [j,n,hR k (k)] ( l=0 (Lk (π n )) ∧ j=0 (Nj (un ) ∧ [α]k ∧ Wm−1 = I l=0 (Nl (un ) ∧ Dm,k;l,j (π n ))∧ Vj > [i,n,hR k (i)] Vk [i,n,hR k (i)] i=0 (Ni (un ) → [β]k ) ∧ i=m [β]k )∨ R I Vk I [j,n,hk (k)] (¬Bk (π n ) ∧ j=m (Dm,j (π n ) → [β]k ))∨ I Vk I [j,n,hRk (k)] (Bk (π n ) ∧ j=m (Dm,j (π n ) → [β]k )∧ Wk−1 l Vk I [j,n,hR k (k)] l=0 [Lk (π n ) ∧ j=l (Dm,k;l,j (π n ) → [β]k )]), [m,n,A] W Wk [j,min(A),gs (A)] Kc α k := s∈ι Is (w0,min(A) ) ∧ j=0 ([α]k ∧Hc (wm,n , wj,min(A) )), [m,n,A] W Wk [j,min(A),gs (A)] DΓ α k := s∈ι Is (w0,min(A) ) ∧ j=0 ([α]k ∧ V H c (w m,n , w j,min(A) )), [m,n,A] Wc∈Γ Wk [j,min(A),gs (A)] EΓ α k := s∈ι Is (w0,min(A) ) ∧ j=0 ([α]k ∧ W c∈Γ H c (w m,n , w j,min(A) )), [m,n,A] DW E[m,n,A] k j CΓ α k := j=1 (E Γ ) α . k Theorem 2. Let M be a model and α be a WECTL∗ KD state formula. Then for some s ∈ ι and for every k ∈ IN, M, s |=k α if, and only if, the propositional formula [M, α]k is satisfiable. 5 Conclusions We have proposed the SAT-based BMC for WECTL∗ KD and for WDIS. The BMC of the WDIS may also be performed by means of Ordered Binary Diagrams (OBDD). This will be explored in the future. Moreover, our future work include an implementation of the algorithm presented here, a careful evaluation of experimental results to be obtained, and a comparison of the OBDD- and SAT-based BMC method for WDIS. References 1. E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7–34, 2001. 2. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999. 3. E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, chapter 16, pages 996–1071. Elsevier Science Publishers, 1990. 4. R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995. 5. X. Huang, C. Luo, and R. van der Meyden. Improved bounded model checking for a fair branching-time temporal epistemic logic. In Proc. of MoChArt 2010, volume 6572 of LNAI, pages 95–111. Springer, 2011. 6. H. Levesque. A logic of implicit and explicit belief. In Proc. of the 6th National Conference of the AAAI, pages 198–202. Morgan Kaufman, 1984. 7. A. Lomuscio and M. Sergot. Deontic interpreted systems. Studia Logica, 75(1):63–92, 2003. 8. Artur Mȩski, W. Penczek, M.Szreter, B. Woźna-Szcześniak, and A. Zbrzezny. BDD- versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. Autonomous Agents and Multi-Agent Systems, 28(4):558–604, 2014. 9. W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167–185, 2003. 10. W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal frag- ment of CTL. Fundamenta Informaticae, 51(1-2):135–156, 2002. 11. W. Penczek, B. Woźna-Szcześniak, and A. Zbrzezny. Towards SAT-based BMC for LTLK over interleaved interpreted systems. Fundamenta Informaticae, 119(3–4):373–392, 2012. 12. M. Pradella, A. Morzenti, and P. San Pietro. A Metric Encoding for Bounded Model Check- ing. In Proc. of FM’2009, volume 5850 of LNCS, pages 741–756. Springer, 2009. 13. M. Wooldridge. An introduction to multi-agent systems - Second Edition. John Wiley & Sons, 2009. 14. B. Woźna. Bounded Model Checking for the universal fragment of CTL*. Fundamenta Informaticae, 63(1):65–87, 2004. 15. B. Woźna, A. Lomuscio, and W. Penczek. Bounded model checking for deontic interpreted systems. In Proc. of LCMAS’2004, volume 126 of ENTCS, pages 93–114. Elsevier, 2005. 16. B. Woźna-Szcześniak. SAT-based bounded model checking for weighted deontic interpreted systems. In Proc. of EPIA’2013, volume 8154 of LNAI, pages 444–455. Springer, 2013. 17. B. Woźna-Szcześniak and A. Zbrzezny. SAT-based BMC for Deontic Metric Temporal Logic and Deontic Interleaved Interpreted Systems. In Post-proc. of DALT’2012, volume 7784 of LNAI, pages 170–189. Springer, 2012. 18. B. Woźna-Szcześniak and A. Zbrzezny. SAT-based bounded model checking for deontic interleaved interpreted systems. In The Proc. of KES-AMSTA’2012, volume 7327 of LNCS, pages 494–503. Springer, 2012. 19. B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. The BMC method for the existen- tial part of RTCTLK and interleaved interpreted systems. In In Proc. of EPIA’2011, volume 7026 of LNAI, pages 551–565. Springer, 2011. 20. B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. SAT-based bounded model check- ing for RTECTL and simply-timed systems. In Proc. of EPEW 2013, volume 8168 of LNCS, pages 337–349. Springer, 2013. 21. B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. SAT-based bounded model check- ing for weighted interpreted systems and weighted linear temporal logic. In Proc. of the PRIMA’2013, volume 8291 of LNAI, pages 355–371. Springer, 2013. 22. B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. Verifying RTECTL properties of a train controller system. Scientific Issues of Jan Dugosz University in Czestochowa: Mathematica, 16:153–162, 2011. 23. A. Zbrzezny. Improving the translation from ECTL to SAT. Fundamenta Informaticae, 85(1-4):513–531, 2008. 24. A. Zbrzezny. A new translation from ECTL∗ to SAT. Fundamenta Informaticae, 120(3- 4):377–397, 2012.