Model Checking BDI Logics over Finite-state Worlds∗

Abstract

Logics with belief, desire and intention attitudes (BDI logics) are among the most widely studied formal languages for modelling rational agents. We consider the logic Ctlb∗di that augments the branching-time logic Ctl∗ with the BDI modalities and adopt the possible-world semantics by Rao and Georgeff. In this paper, we introduce the model-checking problem of Ctlb∗di over finite-state models that are described by tuples of Kripke structures (one for each world) and where the BDI relations are captured by finite-state relations. We then solve the problem by giving an exponential time decision algorithm that is obtained by adapting the standard decision algorithm for Ctl∗.

Introduction

The use of rational agents for modeling real world systems has been heavily investigated and is now well accepted. An architecture that has emerged sees the systems as rational agents having certain mental attitudes of belief, desire, and intention (bdi agents). The beliefs express what the system knows about the state of the environment, the desires capture the information about the objectives to be accomplished and the intentions represent a high-level plan coming with the agent’s commitment to achieve it (intentions force the agent to pursue certain desires) [ 6 ].

bdi agents, and the related specification languages denoted as bdi logics, have received different formulations (see [ 12 ]). Their increasing use in the design and implementation of safety-critical applications has also motivated several approaches to the verification of such models (see [ 4, 5, 3 ]).

Here, we adopt the approach by Rao and Georgeff [ 14, 15 ] based on a possible worlds semantics where each possible world is not an instantaneous state but a transition system: possible worlds share (and are synchronized over) a branching-time structure whose time points represent the instantaneous states. Belief, desire and intentions are expressed through accessibility relations that relate the possible worlds at each time point. These relations can possibly vary over time, which constitutes an important feature for modeling systems (see [ 9 ] and references therein).

In this setting, system properties are expressed by using extensions of Ctl and Ctl∗ [ 8 ] with the belief, desire, and intention modal operators. We denote these logics respectively as Ctlbdi and Ctlb∗di. For Ctlbdi, the model checking question, i.e., determining whether a given model satisfies a given specification, and the satisfiability question, i.e., whether a formula admits a model where it is fulfilled, have been studied respectively in [ 15 ] and in [ 16 ]. In particular, in [ 15 ] a polynomial time decision algorithm is given by restricting the worlds of the system models to have only a finite number of time points.

Although using only a finite number of time points suffices to model some realistic scenarios such as those obtained from scenarios modeled as decision trees (see [ 16 ]), in general this seems to be a serious restriction when dealing with reactive systems that exhibit non-terminating behaviors. In this paper, we thus investigate the model-checking question for bdi branching-time logics and study the model-checking problem for Ctlbdi and Ctlb∗di over finite-state structures that can exhibit infinitely many time points. We assume that models are described as tuples of Kripke structures (one for each world) and the bdi relations are captured by finite-state automata.

Besides the introduction of this new model, as further contributions we give a decision algorithm for the Ctlbdi and the Ctlb∗di model-checking problems. The algorithms are based on the construction of a finite graph obtained as the synchronous cross product of the Kripke structures that define the possible worlds, and the finite automata that express the bdi-accessibility relations. For Ctlbdi, along the same line as for the standard Ctl model-checking algorithm [ 7 ], our algorithm iteratively labels each node u of such graph with the sub-formulas of the input formula that hold true at u. The formulas are processed starting from the atomic propositions and then by increasing number of operators. The only additions to the algorithm from [ 7 ] are the rules that handle the bdi operators. The resulting algorithm takes time linear in the sizes of the graph and the input formula, and thus takes exponential time in the size of the input. For Ctlb∗di, we extend the algorithm just given for Ctlb∗di similarly to how the standard decision algorithm for Ctl∗ is obtained from that of Ctl [ 7 ]. The overall time taken by this algorithm is still exponential in the input size. 2

Branching-time logic with BDI modalities

In this section, we briefly recall the syntax and the semantics of Ctlb∗di [ 15 ].

In the rest of the paper, for an integer k > 0, [k] will denote the set {1, . . . , k}.

Syntax. A Ctlb∗di formula can be a state or a path formula. State formulas are inductively defined starting from atomic propositions by applying the logical connectives, the path quantifiers (to path formulas) and the belief (bel), desire (des), and intention (int) operators. Path formulas are either state formulas or obtained by applying temporal operators such as next ( ) and until (U ). The syntax of Ctlbdi can be obtained from that of Ctlb∗di by disallowing the nesting of Boolean and temporal operators in path formulas. A formal definition for both logics can be found in [ 15 ].

Semantics. The meaning of the formulas from Ctlb∗di, and thus Ctlbdi, is defined according to a possible world semantics where each possible world is not an instantaneous state but a transition system. All the worlds are synchronized over a shared branching-time structure whose time points (nodes) represent the instantaneous states. The meaning of the belief-desire-intention (bdi) operators is given through accessibility relations that relate the possible worlds at each time point and thus can possibly vary over time. The meaning of temporal operators is instead related to the temporal accessibility relation defined by the the branching-time structure.

We start recalling the notion of tree-structure.

For k > 0, a k-ary tree-structure is a pair (T , R) where T ⊆ [k]∗ is a prefix-closed set and R = {(t, t0) | t, t0 ∈ T and t0 = t.i for i ∈ [k]}. The empty word ε denotes the root of the tree. We assume T to be infinite, and refer to the elements of T as time points.

Definition 1. A structure for Ctlb∗di formulas is a tuple M = (AP, T , R, W, B, D, I) where: • AP is a set of atomic propositions; (T , R) is a tree-structure; • W is a set of possible worlds where each world w ∈ W is a tuple (Tw, Rw, Lw) where Tw ⊆ T , Rw is the restriction of R to Tw, (Tw, Rw) is a tree-structure and Lw : Tw → 2AP assigns a set of atomic propositions to each time point of w; • for K ∈ {B, D, I}, K ⊆ W × T × W is such that for (w, t, v) ∈ K, t ∈ Tw ∩ Tv must hold (i.e., bdi accessibility relations are consistently defined with respect to the world time points).

R (resp., B, D, I) is called the temporal (resp., belief, desire, intention) accessibility relation.

A path π in a world w = (Tw, Rw, Lw) is a sequence of time points t0t1 . . . such that (ti, ti+1) ∈ Rw for i ≥ 0. The meaning of formulas is given by the satisfaction relation that is defined starting from a time point for state formulas and along a path for path formulas. We omit here a formal definition which can be obtained along the same lines as for Ctl∗ and just recall the case of bdi operators. For a structure M = (AP, T , R, W, B, D, I), w ∈ W and a time point t: • M, w, t |= belϕ iff for all v ∈ W such that (w, t, v) ∈ B, it must hold M, v, t |= ϕ (similarly for desϕ and intϕ); We say M satisfies a Ctlb∗di formula ϕ at a world w, written M, w |= ϕ, iff M, w, root |= ϕ. Model-checking. We assume that the reader is familiar with the notions of Kripke structure (a finitestate transition system whose states are labeled with atomic propositions) and its tree-unrolling (see [ 7 ]), and finite automaton (see [ 10 ]). For a finite automaton A and a state s, we denote with L(A, s) the language accepted by A assuming s as the sole accepting state (i.e., the language accepted by A is L(A) = S

For thes∈mFoLd(eAl-c,hse)cwkihnegreprFobilse mthewaecccoenpstiidnegr s(e1t) oaf fiAn)i.te number of possible worlds each corresponding to the unrolling of a Kripke structure, and (2) each bdi relation defined by a finite automaton over the paths of the corresponding tree-structures. We refer to such structures as finite-state structures.

We omit a formal definition of above notion and just observe that a finite-state structure M = (AP, T , R, W, B, D, I) has a finite representation of the form (AP, k, W, K¯ , AB, AD, AI , μB, μD, μI ) where: • K¯ = {(Kw, sw) | w ∈ W} and sw is a state for a Kripke structure Kw of arity k for w ∈ W, and • for K ∈ {B, D, I}, AK is finite automaton over time points, μK maps each state of AK to a subset of W × W, and denoting QK the set of states of AK, K = Ss∈QK {(w, t, w0) | (w, w0) ∈ μK(s) and t ∈ L(AK, s) ∩ T }.

In the following, we will denote finite-state structures through their finite representation. Definition 2. Given a finite-state structure M = (AP, k, W, K¯ , AB, AD, AI , μB, μD, μI ), a world w and a Ctlb∗di formula ϕ, the Ctlb∗di model-checking problem asks whether M, w |= ϕ. 3

Decision algorithms

In this section, we discuss our solution to the introduced decision problems.

We start giving the construction of a finite graph that captures the entire input model. This graph essentially consists of the synchronous cross product of the Kripke structures defining the possible worlds along with the finite automata capturing the bdi-accessibility relations. For an input formula ϕ, the decision procedure for Ctlbdi is then obtained by labeling each node of this graph with the ϕ sub-formulas that hold true at it. For this, we adapt the decision algorithm given for the Ctl model-checking (see [ 8 ]) which iteratively label the states of a Kripke structure by considering sub-formulas of increasing sizes. We conclude the section by arguing how to extend the Ctlbdi model-checking algorithm to decide the Ctlb∗di model-checking problem and then discussing the computational complexity of this approach. Construction of the graph GM. For a set of worlds W = {w1, . . . , wn} for n > 0, and a finitestate structure M = (AP, k, W, K¯ , AB, AD, AI , μB, μD, μI ) with K¯ = {(Kw, sw) | w ∈ W} and Kw = (Sw, νw, λw), the graph GM is defined as follows (i, j range over the set {1, . . . , n}, and K ∈ {B, D, I} unless otherwise specified).

The vertices of GM are of the form (wi, s1, . . . , sn, qB, qD, qI ) where: (1) wi denotes the current world, (2) sj either belongs to Kwj and is the current state of world wj or is a dummy state ⊥ denoting that the current one is not a time point of world wj , and (3) qK is the current state of AK.

The edges of GM come from the accessibility relations of M and are labeled consistently: edges derived from the temporal accessibility relation are labeled with a corresponding index from [k] (recall that k is the arity of the Kripke structures) while those derived from the accessibility relation K with a fresh symbol σK for K ∈ {B, D, I}. Formally, denote ν¯w the total function obtained by completing νw by assigning ⊥ whenever it is not defined, i.e., ν¯w(s, j) = ν(s, j) if νw(s, j) is defined and ν¯w(s, j) = ⊥ otherwise . For vertices u = (wi, s1, . . . , sn, qB, qD, qI ) and u0 = (wi0 , s01, . . . , s0n, qB0, qD0, qI0 ) of GM, (u, γ, u0) is an edge of GM iff either one of the following cases holds (we assume that components of u0 equals the corresponding ones from u unless differently specified): • γ ∈ [k], i0 = i, s0j = ν¯wi (sj, γ) for j ∈ [n], and (qK, γ, qK0) is a transition of AK for K ∈ {B, D, I} (we say that u0 is a γ-temporal successor of u); • γ ⊆ {σB, σD, σI }, γ 6= ∅, and for σK ∈ γ, μK(qK) = (wi, wi0 ) [u0 is a K successor of u for each σK ∈ γ.

Note that each vertex of GM has at most k + n successors.

Define λM(u) = λwi (si), for each vertex u = (wi, s1, . . . , sn, qB, qD, qI ) of GM. The labeled graph GM is defined as GM with the labeling function λM. Note that GM differs from Kripke structures only for the distinction of the transitions into temporal and bdi ones.

Properties of GM. We denote τ (GM, u) the tree-structure obtained from GM starting from u and by unrolling the loops of GM.

By τ (GM, u), we can define the satisfiability of Ctlb∗di (and hence of Ctlbdi) formulas w.r.t. GM by treating a formula of the form Kϕ as the corresponding temporal logic formula ∀ ϕ where the universal quantification is restricted to only the K successors of the current vertex. Analogously, standard path quantifiers are restricted to only the temporal successors. The formal definition can be easily obtained from semantics of Ctlb∗di and the observations above. Thus, we omit it here, and again use GM, t |= ϕ (resp., GM, π |= ϕ) meaning that ϕ holds in GM starting from time point t (resp., along path π).

Directly from the given semantics, we have that the Ctlb∗di (resp., Ctlbdi) model-checking problem reduces to the corresponding question on the labeled graph GM. For a world w, we define the initial vertex of GM corresponding to w the only vertex of the form (w, sw1 , . . . , swn , qB0, q0 , q0 ) where q0 is the initial state of AK for K ∈ {B, D, I} (recall that each swi is the state coupled with the Kripke stKructure D I Kwi in the finite-state structure we have fixed earlier in this section).

Lemma 1. For a world w and a Ctlb∗di formula ϕ, we get that M, w |= ϕ iff GM, u |= ϕ, where u is the initial state of of GM corresponding to w.

A crucial property of GM is that as for standard Kripke structures the truth of branching-time state formulas depends only on the state, i.e., a state formula ϕ is true at a time point t of τ (GM, u) if and only if it is true at any other time point t0 such that t and t0 correspond to the same vertex of GM. To see this, for a k-ary tree-structure (T , R), we define the abstract subtree rooted at t ∈ T as the k-ary tree-structure (T 0, R0) where T 0 = {t0 | t.t0} and R0 = {(t0, t0.i) ∈ R | t0 ∈ T 0}. Thus, directly from the definition of τ (GM, u), we get that the abstract sub-trees rooted at t and t0 coincide for all time points t, t0 of τ (GM, u) that correspond to the same vertex of GM and hence the property stated above holds. Lemma 2. Given a Ctlb∗di state formula ϕ, for all time points t, t0 of τ (GM, u) that correspond to the same vertex of GM we get: τ (GM, u), t |= ϕ iff τ (GM, u), t0 |= ϕ.

Decision algorithms. Lemma 2 allows us to give for our model-checking questions two fixed-point decision algorithms in the style of those given for Ctl and Ctl∗. Such algorithms proceed bottom-up on the syntactic structure of ϕ and starting from the labeling given by the truth of the atomic propositions, progressively label each vertex u of the graph with the sub-formulas that holds true there. The rules of the algorithm for Ctlbdi, denoted Alg-Ctlbdi, are given in Figure 1.

To get a decision algorithm for Ctlb∗di we can reason similarly to how a decision algorithm Ctl∗ is obtained from that for Ctl (see [ 7 ] for details). In particular, for a path formula ϕ denote with ϕ0 the formula obtained by replacing in ϕ its state sub-formulas with new atomic propositions. Thus, the truth of ϕ at a vertex u of GM is determined by a query to an Ltl model-checking algorithm on ϕ0 by taking for the added atomic proposition the evaluation given by lab to the corresponding state formulas. We denote with Alg-Ctlb∗di the resulting algorithm. The correctness of algorithms Alg-Ctlbdi and Alg-Ctlb∗di is a consequence of Lemmas 1 and 2, and the above observations. Thus we have:

Initialization.

For each vertex u of GM, set lab(u) = λM(u).

Update rules.

For each vertex u of GM: 1. if ϕ = ¬ψ, then ϕ ∈ lab(u) iff ψ 6∈ lab(u); 2. if ϕ = ϕ1 ∨ ϕ2 then ϕ ∈ lab(u) iff either ϕ1 ∈ lab(u) or ϕ2 ∈ lab(u); 3. if ϕ = ∃

ψ ∈ lab(u0); 4. if ϕ = ∀ ψ ∈ lab(u0); ψ, then ϕ ∈ lab(u) iff there is a temporal successor u0 of u such that ψ, then ϕ ∈ lab(u) iff for all temporal successors u0 of u it holds that 5. if ϕ = ∃(ϕ1U ϕ2), then ϕ ∈ lab(u) iff either ϕ2 ∈ lab(u), or ϕ1 ∈ lab(u) and there is

a temporal successor u0 of u such that ϕ ∈ lab(u0); 6. if ϕ = ∀(ϕ1U ϕ2), then ϕ ∈ lab(u) iff either ϕ2 ∈ lab(u), or ϕ1 ∈ lab(u) and for all

temporal successors u0 of u it holds that ϕ ∈ lab(u0); 7. if ϕ = belψ, then ϕ ∈ lab(u) iff for all B successors u0 of u it holds that ψ ∈ lab(u0)

(similarly for desϕ and intϕ).

Lemma 3. Given a Ctlbdi (resp., Ctlb∗di) state formula ϕ, a finite-state structure M and a world w, M, w |= ϕ iff ϕ ∈ lab(u) where lab is the labeling computed by Alg-Ctlbdi (resp., Alg-Ctlb∗di) and u is the initial state of of GM corresponding to w.

Computational complexity. We observe that the construction o·ηf3G)Mwhcearueseχs iasntheexpmoanxeinmtuiamlbnluowm-buepr in the size of M. In fact, the number of vertices of GM is O(n · χn of states over the n Kripke structures denoting the possible worlds of M and η is the maximum number of states over the finite-state automata denoting the bdi accessibility relations of M. Moreover, for each vertex of GM there are at most k + n outgoing edges where k is the arity of the Kripke structures. Thus, the overall number of GM edges is O(k · n2 · χn · η3). For a formula ϕ the number of its sub-formulas is linear in the size of ϕ (denoted |ϕ|). Thus the fixed-point algorithm Alg-Ctlbdi will converge in at most O(|ϕ| · k · n2 · χn · η3) steps, and since each step require at most O(n) time, we get the following result. Theorem 1. The Ctlbdi model-checking problem can be solved in time exponential in the number of the worlds, and polynomial in the size of the formula and the size of the automata capturing the bdi relations.

Since Ltl model-checking can be solved in time exponential in the size of the formula and linear in the size of the model [ 13 ], Alg-Ctlb∗di requires exponential time also in the size of the formula. Theorem 2. The Ctlb∗di model-checking problem can be solved in time exponential in the number of worlds and the size of the formula, and polynomial in the size of the automata capturing the bdi relations. 4

Conclusions

In this paper, we have presented some preliminary results on the model-checking problem of Ctlbdi and Ctlb∗di over finite-state models. We have shown that these decision problems are decidable in time exponential in both the size of the input model and the size of the input formula. Our results extend the decidability of the considered logics to systems that exhibit infinitely many time points resulting from the unrolling of the finite-state models.

As future research, we wish to investigate further the considered decision problems. First, we will look deeper into their computational complexity and possibly show tight complexity bounds for the problems stated in this paper. Second, we will consider modular descriptions of systems where each world is composed of modules that can call each other possibly recursively, similarly to what is done for standard temporal logics (see [ 1, 11, 2 ]). This will give a more faithful representation for many real systems and will yield more succinct models (modules can be shared among worlds). Moreover, the presence of recursive calls will extend further the class of models considered for the logics Ctlbdi and Ctlb∗di.

References

[1] R. Alur , M. Benedikt , K. Etessami , P. Godefroid , T. W. Reps , and M. Yannakakis . Analysis of recursive state machines . ACM Trans. Program. Lang. Syst. , 27 ( 4 ): 786 - 818 , 2005 .

[2] B. Aminof , O. Kupferman , and A. Murano . Improved model checking of hierarchical systems . Inf. Comput. , 210 : 68 - 86 , 2012 .

[3] M. Benerecetti , F. Giunchiglia , and L. Serafini . Model checking multiagent systems . J. Log. Comput. , 8 ( 3 ): 401 - 423 , 1998 .

[4] J. Blee , D. Billington , G. Governatori, and A. Sattar . Levels of modality for BDI logic . J. Applied Logic , 9 ( 4 ): 250 - 273 , 2011 .

[5] R. H. Bordini , M. Fisher, W. Visser, and M. J. Wooldridge . Verifying multi-agent programs by model checking . Autonomous Agents and Multi-Agent Systems , 12 ( 2 ): 239 - 256 , 2006 .

[6] M. E. Bratman . Intentions, plans, and practical reason. Harvard University Press, 1987 .

[7] E. A. Emerson . Temporal and modal logic . In Handbook of Theoretical Computer Science , Volume B: Formal Models and Sematics (B), pages 995 - 1072 . The MIT Press/Elsevier, 1990 .

[8] E. A. Emerson and E. M. Clarke . Using branching time temporal logic to synthesize synchronization skeletons . Sci. Comput. Program. , 2 ( 3 ): 241 - 266 , 1982 .

[9] J. Y. Halpern and M. Y. Vardi . The complexity of reasoning about knowledge and time. i. lower bounds . J. Comput. Syst. Sci. , 38 ( 1 ): 195 - 237 , 1989 .

[10] J. E. Hopcroft , R. Motwani , and J. D. Ullman . Introduction to automata theory, languages, and computation - (2 . ed.). Addison-Wesley series in computer science . Addison-Wesley-Longman , 2001 .

[11] S. La Torre , M. Napoli , M. Parente , and G. Parlato . Verification of scope-dependent hierarchical state machines . Inf. Comput. , 206 ( 9 -10): 1161 - 1177 , 2008 .

[12] J.-J. C. Meyer , J. Broersen, and A. Herzig . Bdi logics . In Handbook of Epistemic Logic , pages 453 - 498 . College Publications, 2015 .

[13] A. Pnueli . The temporal logic of programs . In 18th Annual Symposium on Foundations of Computer Science , Providence, Rhode Island, USA, 31 October - 1 November 1977 , pages 46 - 57 , 1977 .

[14] A. S. Rao and M. P. Georgeff . Modeling rational agents within a bdi-architecture . In J. F. Allen, R. Fikes , and E. Sandewall, editors, Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR'91) . Cambridge, MA, USA, April 22 - 25 , 1991 ., pages 473 - 484 . Morgan Kaufmann, 1991 .

[15] A. S. Rao and M. P. Georgeff . A model-theoretic approach to the verification of situated reasoning systems . In R. Bajcsy, editor, Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry , France, August 28 - September 3 , 1993 , pages 318 - 324 . Morgan Kaufmann, 1993 .

[16] A. S. Rao and M. P. Georgeff . Decision procedures for BDI logics . J. Log. Comput. , 8 ( 3 ): 293 - 342 , 1998 .