SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems (Extended Abstract) ?

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. ? Partly supported by National Science Center under the grant No. 2011/01/B/ST6/05317.

-

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 epistemic properties. The formalism of deontic interpreted systems (DIS) [ 7 ] is an extension of ISs, which makes possible reasoning about temporal, epistemic and correct functioning 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 temporal, 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 propositional 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 satisfying 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 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 together 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.

Related work. Figure 1 provides diagram showing the relations between classical temporal 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 models 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 temporal logics with discrete semantics over weighted Kripke models generated, for example, 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 fusion 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 defined 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

A path in M is an infinite sequence = s0 a!1 s1 a!2 s2 a!3 : : : of transitions. For such a path, and for j 6 m 2 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: m = sm am!+1 sm+1 am!+2 sm+2 : : :. Next, by [j::m] we denote the finite sequence sj aj!+1 sj+1 aj!+2 : : : 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 when j = m). By (s) we denote the set of all the paths starting at s 2 S, and by (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: propositional variables; the boolean operators (^-conjunction, _-disjunction, :-negation); the temporal modalities (XI -weighted next step, UI -weighted until, RI -weighted release, 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 modalities (Oc and Kb cc12 representing the correctly functioning circumstances of agents). Syntax of WECTL KD. Let p 2 PV be a propositional variable, c; c1; c2 2 Ag, Ag, and I be an interval in IN = f0; 1; 2; : : :g of the form: [a; b) and [a; 1), for a; b 2 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: ' ::=true j false j p j :p j ' ^ ' j ' _ ' j E j Kc j E j D j C ::=' j ^ j _ j XI j

UI j RI ing definitions of epistemic relations: closure of E ), Dd=ef T

c, where 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 followE d=ef S c, C d=ef ( E )+ (the transitive c2

Ag.

c2 Definition 1. Let M be a model, s a state of M , a state formula over PV, the notation M; s j= a path in M , and m 2 IN. For means that holds at the state j Oc j Kb cc12 s in the model M . Similarly, for a path formula ' over PV, the notation M; j= ' means that ' holds along the path in the model M . Moreover, let p 2 PV be a propositional variable, , be state formulae of WECTL KD, and ', be path formulae of WECTL KD. The relation j= is defined inductively as follows: M; s j= true, M; s 6j= false, M; s j= p iff p 2 V(s), M; s j= :p iff p 2= V(s), M; s j= ^ iff M; s j= and M; s j= , M; s j= _ iff M; s j= or M; s j= , M; s j= Kc iff (9 2 )(9i > 0)(s c (i) and M; i j= ), M; s j= Y iff (9 2 )(9i > 0)(s Y (i) and M; i j= ); Y 2 fD; E; Cg, M; s j= Oc iff (9 2 )(9i > 0)(s /c (i) and M; i j= ), M; s j= Kb cc12 iff (9 2 )(9i > 0)(s c1 (i) and s /c2 (i) and M; i j= ), M; s j= E' iff (9 2 (s))(M; 0 j= '), M; m j= iff M; (m) j= , M; m j= ' ^ iff M; m j= ' and M; m j= , M; m j= ' _ iff M; m j= ' or M; m j= , M; m j= XI ' iff D [m::m + 1] 2 I and M; m+1 j= ', M; m j= 'UI iff (9j > m) D [m::j] 2 I and M; j j= and

(8m 6 i < j)M; i j= ' , M; m j= 'RI iff (9j > m) D [m::j] 2 I and M; j j= ' and (8m 6 i 6 j)

M; i j= or (8j > m)(D [m::j] 2 I implies M; j j= ).

A WECTL KD state formula is true in the model M , denoted by M j= , iff for some s 2 , M; s j= , i.e., holds at some initial state of M . The model checking problem asks whether M j= .

Bounded semantics of WECTL KD. A bounded semantics for WECTL KD is the basis of the translation of bounded model checking problem to the satisfiability of propositional 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 2 IN a bound, and 0 6 l 6 k. A k-path l is a pair ( ; l), where is a finite sequence s0 a!1 s1 a!2 : : : a!k 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!, where u = (s0 a!1 s1 a!2 : : : a!l sl) and v = (sl+1 al!+2 : : : a!k sk). k(s) denotes the set of all the k-paths of M that start at s, and k = Ss02 k(s0).

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 j=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 j=k ', where 0 6 m 6 k, denotes that the formula ' is k-true along the suffix (m) am!+1 (m + 1) am!+2 : : : a!k (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 2 PV a propositional variables, , state formulae of WECTL KD, and ', path formulae of WECTL KD. The relation j=k is defined inductively as follows: M;s j=k true; M;s 6j=k false, M;s j=k p iff p 2 V(s); M;s j=k :p iff p 2= V(s), M;s j=k ^ iff M;s j=k and M;s j=k , M;s j=k _ iff M;s j=k or M;s j=k , M;s j=k Kc iff (9 l 2 k)(90 6 j 6 k)(M; lj j=k and s c (j)), M;s j=k Y iff (9 l 2 k)(90 6 j 6 k)(M; lj j=k and s Y (j)), where Y 2 fD;E;Cg, M;s j=k Oc iff (9 l 2 k)(90 6 j 6 k)(M; lj j=k and s /c (j)), M;s j=k Kbcc12 iff (9 l 2 k)(90 6 j 6 k)(M; lj j=k and s c1 (j) and s /c1 (j)), M;s j=k E' iff (9 l 2 k(s))(M; l0 j=k '), M; lm j=k iff M; (m) j=k , M; lm j=k ' ^ iff M; lm j=k ' and M; lm j=k , M; lm j=k ' _ iff M; lm j=k ' or M; lm j=k , M; lm j=k XI' iff (m < k and D [m::m + 1] 2 I and M; lm+1 j=k ') or (m = k and l < k and (k) = (l) and D [l::l + 1] 2 I and M; ll+1 j=k '), M; lm j=k 'UI iff (9m 6 j 6 k)(D [m::j] 2 I and M; lj j=k and (8m 6 i < j)M; li j=k ')or(l < m and (k) = (l) and (9l < j < m)(D [m::k] + D [l::j] 2 I and M; lj j=k and (8l < i < j)M; li j= ' and (8m 6 i 6 k)M; li j=k ')), M; lm j=k 'RI iff (D [m::k] > right(I) and (8m 6 j 6 k)(D [m::j] 2 I implies M; lj j=k )) or (D [m::k] < right(I) and (k) = (l) and (8m 6 j 6 k)(D [m::j] 2 I implies M; lj j=k ) and (8l 6 j 6 k)(D [m::k] + D [l::j] 2 I implies M; lj j=k )) or (9m 6 j 6 k)(D [m::j] 2 I and M; lj j=k ' and (8m 6 i 6 j)M; li j=k ) or (l < m and (k) = (l) and (9l < j < m)(D [m::k] + D [l::j] 2 I and M; lj j=k ' and (8l < i 6 j)M; li j= and (8m 6 i 6 k)M; li j=k )).

A WECTL KD state formula is k-true in M, denoted M j=k ', iff for some s 2 , M;s j=k '. The bounded model checking problem asks whether there exists k 2 IN such that M j=k '.

Lemma 1. Let M be a model, s a state of M, and a WECTL KD state formula. for some k 2 IN, if M;s j=k , then M;s j= . if M;s j= , then M;s j=k for some k 2 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 2 , M;s j= iff M;s j=k for some k 2 IN.

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 j=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 2 Ag [ fE g. Then, each state s = (`1; : : : ; `n; `E ) 2 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 ) 2 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 propositional 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 : f0; 1g P V ! P V [ f:q j q 2 P V g is a function defined as: lit(1; q) = q and lit(0; q) = :q.

V : P V ! f0; 1g 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; : : : ; dr1d1 ; : : : ; d1n+1; : : : ; drnd+(n1+1) ), where rd1; : : : ; rd(n+1) denote lengths of local symbolic weights.

For every rw; ra; rd 2 IN+, each valuation V induces the functions S : SV rw ! f0; 1grw , A : AV ra ! f0; 1gra , W : W V rd ! IN, and J : N V y ! IN defined 2i 1, J((u1; : : : ; uy)) = Py

i=1 V (ui) 2i 1.

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 2 V(S(w)). It encodes a set of states of M in which p 2 PV holds.

Is(w) = Vir=w1 lit(s[i]; wi). This Boolean formula is defined over SV (w), and it encodes the state s of the model M .

H(w; w0) = Vir=w1 wi , w0i. 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 valuation V 2 f0; 1gSV 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 2 Ag [ fE g and a 2 Actc [ f"g is a Boolean formula over AV (ac) that is true for each valuation V 2 f0; 1gAV such that V satisfies Ha(ac) iff A(ac) = a.

A(a) = Va2Act(Vc2Ag(a) Ha(ac) _ Vc2Ag(a) H"(ac)), where Ag(a) = fc 2 Ag [ fE g j a 2 Actcg. 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); w0c) is defined over SV (wc) [ SV (w0c), and is true for a valuation V iff tc(S(wc); A(a)) = S(w0c). This Boolean formula encodes the local evolution function of agent c.

T (w; (a; d); w0) = Vc2Ag[fEg 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 .

Njs(u) is a formula over N V (u) that is true for a valuation V iff j s J(u), where s2 f<; >; 6; =; >g. This formula encodes that the value j is in the arithmetic relation s 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 2 PV. To calculate the number, we define the following auxiliary function fk : WECTL KD ! IN: fk(true) = fk(false) = 0, fk(p) = fk(:p) = 0, fk('^ ) = fk(')+fk( ), fk('_ ) = maxffk('); fk( )g, fk(XI ') = fk('), fk('UI ) = k fk(')+fk( ), fk('RI ) = (k+1) fk( )+fk('), fk(C ') = fk(') + k, fk(Y ') = fk(') + 1, for Y 2 fKc; D ; E ; Oc; Kb cc12 ; Eg.

Furthermore, we define the j-th symbolic k-path j as the sequence of symbolic transitions: (w0;j a1;j!;d1;j w1;j a2;j!;d2;j : : : ak;j!;dk;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; 1), for a; b 2 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).

Bk( n) is defined over Sik=1 W V (di;n), and is true for a valuation V iff

I Pk

i=1 W(di;n) 6 right(I). This Boolean formula encodes that the weight represented by the sequence d1;n; : : : ; dk;n is less than or equal to right(I). DaI;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 for a valuation V iff Pb

i=a+1 W(di;n) 2 I; otherwise, i.e. if a = b, then DaI;b( n) is true for a valuation V iff 0 2 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. the formula is true for a valuation V iff Pb i=c+1W(di;n) 2 I; i=a+1W(di;n)+Pd 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 for a valuation V iff Pd

i=c+1 W(di;n) 2 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 for a valuation V iff Pb i=a+1 W(di;n) 2 I;

I 4. if a = b and c = d, then Da;b;c;d( n) is true for a valuation V iff 0 2 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 [M ; ]k := _ Is(w0;0) ^ ^ _ Nl=(uj ) ^ s2 j=1 l=0 fk( ) k 1 ^ ^ j=1 i=0

T (wi;j ; (ai;j ; di;j ); wi+1;j ) where wi;j , ai;j , di;j , and uj are, respectively, symbolic states, symbolic actions, symbolic 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 propositional formula [ ]M;k. In order to define [ ]M;k, we have to know how to divide the set A of k-paths such that jAj = fk( ) into subsets needed for translating the subformulae 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 2 A and y 2 B, then x < y. Further, let A IN be a finite non-empty set, and n; m 2 IN, where m 6 jAj. Then, gl(A; m) denotes the subset B of A such that jBj = m and B A n B, gr(A; m) denotes the subset C of A such that jCj = m and A n C C, gs(A) denotes the set A n fmin(A)g, and if n divides jAj m, then hp(A; m; n) denotes the sequence (B0; : : : ; Bn) of subsets of A such that Sn j=0 Bj = A, jB0j = : : : = jBn 1j, jBnj = m, and Bi Bj for every 0 6 i < j 6 n. Now let hkU(A; m) := hp(A; m; k) and hR(A; m) := hp(A; m; k +1). Note that if hkU(A; m) = (B0; : : : ; Bk), k then hU(A; m)(j) denotes the set Bj , for every 0 6 j 6 k. Similarly, if hkR(A; m) = k (B0; : : : ; Bk+1), then hkR(A; m)(j) denotes the set Bj , 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 2 fE; Kc; D ; E ; Oc; Kb cc12 g: for a given WECTL KD formula Q', if the set A is 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 hkU 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(A; fk( ))(k) 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(A; fk( ))(i) is used to translate k the formula ' along the symbolic path n with starting point i. Notice that if k does not divide jAj d, then hkU(A; d) is undefined. However, for every set A such that jAj = fk('UI ), it is clear from the definition of fk that k divides jAj fk( ).

The function hkR 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 hkR(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(A; fk('))(i) is used to translate k the formula along the symbolic path n with starting point i. Notice that if k + 1 does not divide jAj 1, then hkR(A; p) is undefined. However, for every set A such that jAj = fk('RI ), it is clear from the definition of fk that k + 1 divides jAj fk(').

Let be a WECTL KD state formula and A IN+ be a set of numbers of symbolic [m;n;A] we k-paths such that jAj = fk( ). If n 2 IN n A and 0 6 m 6 k, then by h ik 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 jBj = fk('). If n 2 IN+ n A and 0 6 m 6 k, [m;n;A] we denote the translation of a WECTL KD path formula ' along the then by [']k symbolic k-path n with starting point m by using the set A. Furthermore, we define [0;0;Fk( )], where Fk( ) = fj 2 IN j 1 6 j 6 fk( )g, and: [ ]M;k as h[m;ink;A] := true; hfalseik htrueik [m;n;A] := false;

[m;n;A] := p(wm;n); hpik

[m;n;A] := :p(wm;n); h:pik hhhE'^_i[kmii;[[kknmm;A;;nn];;AA]] :::=== hhH(iiw[[kkmmm;;nn;n;;gg;ll((wAA0;;ff;mkk((in))())A]] )^_) ^hh [ii'[[kkmm][k0;;nn;m;;ggirrn(((AAA;;)ff;kkgs((( A)))))]]],,, [ ][km;n;A] := h i[km;n;A], [' ^ ][km;n;A] := ['][km;n;gl(A;fk('))] ^ [ ][km;n;gr(A;fk( ))]; [' _ ][km;n;A] := ['][km;n;gl(A;fk('))] _ [ ][km;n;gr(A;fk( ))], ( I

Dm;m+1( n) ^ [ ][km+1;n;A];

Wlk=01(DlI;l+1( n) ^ Llk( n) ^ [ ][kl+1;n;A]); [XI ][km;n;A] := if m < k if m = k [ UI ][km;n;A] := Wjk=m(DmI;j ( n) ^ [ ][kj;n;hkU(k)] ^ Vij= m1[ ][ki;n;hkU(i)])_ (WWmlm=011 Llk( n)) ^ WIjm=01(Nj>(un) ^ [ ][kj;n;hkU(k)]^

l=0 (Nl=(un) ^ Dm;k;l;j ( n))^ Vij=0 (Ni>(un) ! [ ][ki;n;hkU(i)]) ^ Vik=m[ ][ki;n;hkU(i)]),

1 [ RI ][km;n;A] := Wjk=m(DmI;j ( n) ^ [ ][kj;n;hkR(k)] ^ Vij=m[ ][ki;n;hkR(i)])_ Wlm=01(Nl=(un) ^ DmIj;=k;0l;j((Nj>n)()u^n) ^ [ ][kj;n;hkR(k)]^ (Wlm=01(Llk( n)) ^ Wm 1 Kc D E C

Vij=0(Ni>(un) ! [ ][ki;n;hkR(i)]) ^ Vik=m[ ][ki;n;hkR(i)])_

I j=m(DmI;j ( n) ! [ ][kj;n;hkR(k)]))_ (:Bk( n) ^ Vk

j=m(DmI;j ( n) ! [ ][kj;n;hkR(k)])^ (BkI( n) ^ Vk

Wk 1 j=l(DmI;k;l;j ( n) ! [ ][j;n;hkR(k)])]), [km;n;A] := Wls=20 I[Ls(lkw( 0;nm)in^(AV))k ^ Wjk=0([ ][kj;min(A);gsk(A)]

^Hc(wm;n; wj;min(A))), [m;n;A] := W k ^

j=0([ ][j;min(A);gs(A)] Vs2 Is(w0;min(A)) ^ Wk k c2 Hc(wm;n; wj;min(A))),

j=0([ ][j;min(A);gs(A)] Ws2 Is(w0;min(A)) ^ Wk k ^ [m;n;A] := W k

c2 [m;n;A] := DWk k j=1(E )

Hc(wm;n; wj;min(A))), j E[m;n;A]

.

k Theorem 2. Let M be a model and s 2 and for every k 2 IN, M; s j=k is satisfiable. 5 Conclusions be a WECTL KD state formula. Then for some if, and only if, the propositional formula [M; ]k 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 Me¸ski, W. Penczek, M. Szreter , B. Woz´na-Szczes´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. Woz´na, and A. Zbrzezny . Bounded model checking for the universal fragment of CTL . Fundamenta Informaticae , 51 ( 1-2 ): 135 - 156 , 2002 .

11. W. Penczek , B. Woz´na-Szczes´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 Checking . 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. Woz´na. Bounded Model Checking for the universal fragment of CTL* . Fundamenta Informaticae , 63 ( 1 ): 65 - 87 , 2004 .

15. B. Woz´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. Woz´na-Szczes´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. Woz´na-Szczes´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. Woz´na-Szczes´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. Woz´na-Szczes´niak, A. M. Zbrzezny, and A. Zbrzezny . The BMC method for the existential part of RTCTLK and interleaved interpreted systems . In In Proc. of EPIA' 2011 , volume 7026 of LNAI , pages 551 - 565 . Springer, 2011 .

20. B. Woz´na-Szczes´niak, A. M. Zbrzezny, and A. Zbrzezny . SAT-based bounded model checking for RTECTL and simply-timed systems . In Proc. of EPEW 2013 , volume 8168 of LNCS , pages 337 - 349 . Springer, 2013 .

21. B. Woz´na-Szczes´niak, A. M. Zbrzezny, and A. Zbrzezny . SAT-based bounded model checking 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. Woz´na-Szczes´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 .