bdi agents are among the most widely studied models of rational agents. In this architecture, systems are seen as rational agents with certain mental attitudes such as belief, desire, and intention. In this paper, we consider the model-checking problem for Ctlbdi, the branching-time logic Ctl augmented with the BDI modalities, over finite-state structures, and in particular, a proof-ofconcept tool that is based on a translation to a formula in a fixed-point logic. We give a description of this tool in some details and also discuss some preliminary evaluations.
Λ(σ, ψ, u) := Λaσt ∨ Λσ¬ ∨ Λσ∨ ∨ Λ∀σ ∨ Λ∃σ ∨ Λ∀σU ∨ Λ∃σU ∨ ΛσB ∨ ΛσD ∨ ΛIσ where: 1. Λ0at := Atomic(ψ) ∧ ¬Label(ψ, u) 2. Λ1at := Atomic(ψ) ∧ Label(ψ, u) 3. Λσ¬ := Neg(ψ) ∧ ∃ψ0.( Ready(ψ0, u) ∧ Sub(ψ0, ψ) ∧ Λ(1 − σ, ψ0, u) ) 4. Λσ∨ := Or(ψ)
∧∃ψ0,ψ00. (Ready(ψ0)∧Sub(ψ0, ψ)∧Ready(ψ00)∧Sub(ψ00, ψ)∧(Λ(σ, ψ0, u) oσΛ(σ, ψ00, u)) ), where oσ is ∨ if σ = 1 and ∧ otherwise 5. Λ0 := Existential(ψ) ∧ Next(ψ) ∃
∧ ∃ψ0. ( Ready(ψ0) ∧ Sub(ψ0, ψ) ∧ ∀v. ( ¬SuccT (v, u) ∨ Λ(0, ψ0, v) ) ) 6. Λ1 := Existential(ψ) ∧ Next(ψ) ∃
∧ ∃ψ0. ( Ready(ψ0) ∧ Sub(ψ0, ψ) ∧ ∃v. ( SuccT (v, u) ∧ Λ(1, ψ0, v) ) ) 7. Λ0 := Universal(ψ) ∧ Next(ψ) ∀
∧ ∃ψ0. ( Ready(ψ0) ∧ Sub(ψ0, ψ) ∧ ∃v. ( SuccT (v, u) ∧ Λ(0, ψ0, v) ) ) 8. Λ1 := Universal(ψ) ∧ Next(ψ) ∀
∧ ∃ψ0. ( Ready(ψ0) ∧ Sub(ψ0, ψ) ∧ ∀v. ( ¬SuccT (v, u) ∨ Λ(1, ψ0, v) ) ) 9. Λ0∃U := Existential(ψ) ∧ Until(ψ) ∧ ∃ψ0, ψ00. ( Ready(ψ0) ∧ Ready(ψ00) ∧ Sub(ψ0, ψ00, ψ) ∧ Λ(0, ψ00, u)
∧ ( Λ(0, ψ0, u) ∨ ∀v. ( ¬SuccT (v, u) ∨ Λ(0, ψ, v) ) ) ) 10. Λ1∃U := Existential(ψ) ∧ Until(ψ) ∧ ∃ψ0, ψ00. ( Ready(ψ0) ∧ Ready(ψ00) ∧ Sub(ψ0, ψ00, ψ)
∧ ( Λ(1, ψ00, u) ∨ ( Λ(1, ψ0, u) ∧ ∃v. ( SuccT (v, u) ∧ Λ(1, ψ, v) ) ) ) ) 11. Λ0 := Universal(ψ) ∧ Until(ψ) ∀U ∧ ∃ψ0, ψ00. ( Ready(ψ0) ∧ Ready(ψ00) ∧ Sub(ψ0, ψ00, ψ) ∧ Λ(0, ψ00, u)
∧ ( Λ(0, ψ0, u) ∨ ∃v. ( SuccT (v, u) ∧ Λ(0, ψ, v) ) ) ) 12. Λ1∀U := Universal(ψ) ∧ Until(ψ) ∧ ∃ψ0, ψ00. ( Ready(ψ0) ∧ Ready(ψ00) ∧ Sub(ψ0, ψ00, ψ)
∧ ( Λ(1, ψ00, u) ∨ ( Λ(1, ψ0, u) ∧ ∀v. ( SuccT (v, u) ∧ Λ(1, ψ, v) ) ) ) ) 13. Λ0 := bel(ψ) ∧ ∃ψ0. ( Ready(ψ0) ∧ Sub(ψ0, ψ) ∧ ∃v. ( SuccB(v, u) ∧ Λ(0, ψ0, v) ) )
(siBmilarly for desire and intention formulas) 14. Λ1 := bel(ψ) ∧ ∃ψ0. ( Ready(ψ0) ∧ Sub(ψ0, ψ) ∧ ∀v.( ¬SuccB(v, u) ∨ Λ(1, ψ0, v) ) ) (siBmilarly for desire and intention formulas)
Syntax. Ctlbdi formulas are inductively defined starting from atomic propositions by applying the logical connectives, the path quantifiers coupled with a temporal operator such as next ( ) and until (U), and the belief (bel), desire (des), and intention (int) operators.
Semantics. The meaning of the formulas from 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 then given through accessibility relations that relate the possible worlds at each time point and thus can possibly vary over time, while the meaning of temporal operators is related to the temporal accessibility relation defined by the the branching-time structure.
A finite-state structure constrains a general Ctlbdi structure such that: • the shared branching-time structure is a full k-ary tree for an integer k > 0 (i.e., an infinite tree where each node has exactly k children), • each of the worlds is defined by a Kripke structure whose tree unrolling from its unique initial state is contained into the shared branching time structure (i.e., each transition is mapped to a child from 1 through k and from each state there is at most an outgoing transition corresponding to a given child i), • each bdi relation is defined by a finite automaton that takes as input sequences over the alphabet {1, . . . , k}, i.e., an automaton that maps paths of the tree-structure to the worlds modeling the bdi attitude.
For a structure M, a world w and a Ctlbdi formula ϕ we denote that ϕ is fulfilled on M starting from w as M, w |= ϕ.
Model-checking. The Ctlbdi model-checking problem over finite-state structures asks whether M, w |=
ϕ holds for given finite-state structure M, world w and Ctlbdi formula ϕ. In [
Figure 1 gives the relation that captures the labeling of GM nodes with the fulfilled sub-formulas. This definition uses predicates to denote the successors in the graph GM, to relate formulas to sub-formulas, and to denote whether a sub-formula is an atomic proposition, the negation/disjunction of formulas, universally/existentially quantified, a next/until/belief/desire/intention formula. Additionally, Ready(ψ, u) denotes the formula ∃σ.Λ(σ, ψ, u).
In particular, the following theorem holds:
Theorem 1. [
M, w |= ϕ iff Λ(1, ϕ, u) holds true where u is the initial state of GM corresponding to w. 3
In this section we give an overview of a prototype tool called bdi-checker for solving the model-checking
problem of Ctlbdi. The underling search space engine uses Binary Decision Diagrams to implement the
algorithm’s operations as well as to represent the set of reachable states during the analysis. To illustrate
our translation we consider a case study taken from [
Case study. We consider a simple scenario where a robot can essentially perform two tasks: getting a beer from the refrigerator and opening the door. The only uncertainties in the environment are the presence or not of a beer can in the refrigerator and of a person at the door house. We can model these as beliefs and thus have four different Kripke structures one for each of the possible beliefs.
In the beginning, all the beliefs are possible and thus all the worlds are belief-accessible. As soon as the robot realizes that no beer is in the refrigerator only the two worlds matching this belief become accessible. Also, if the doorbell rings, the robot changes its beliefs about the presence of a person at the
• Transition systems nodes • AP labeling • temporal, belief, desire, intention successors • Subformula representation • Subformula relation • Subformula types
Predicates Fixed-point algorithm
YES/NO counterexample house door. After opening the door, the robot becomes again agnostic on whether there is a person at the door. After sensing that no beer is in the refrigerator instead its beliefs about the content of the refrigerator will not change forever (this might be changed by adding a further event that a delivery man brings some beer cans).
Robot desires and intentions can be modeled by adding more worlds “refining” the belief related worlds. To keep the description simple, in this version of the paper we omit a detailed discussion of such aspects.
We consider two Ctlbdi formulas: ϕ1 = ∀ ( bel br → ∃ bb), i.e., “whenever the robot believes that a beer can is in the refrigerator, she can possibly bring it back”, and ϕ2 = ∀ ( bel br → ∃ bb ), i.e., “whenever the robot believes that a beer can is in the refrigerator, she can always bring it back”. The first one is fulfilled on our structure, while the second one is not.
Architecture. The tool architecture is shown in Figure 2. bdi-checker takes as input a finite-state structure M and a Ctlbdi formula ϕ, and returns as result “YES”, if the model M meets the specification ϕ, and a counter-example witnessing that M does not satisfy ϕ, otherwise.
The first internal module of bdi-checker, called TRANSLATION INTO PREDICATES, takes as input M and ϕ and transforms them into a series of definitions of Boolean predicates. In particular, we define the predicates used in the definition of formula Λ given in Figure 1: we encode the nodes of graph GM from the Kripke structures and the automata of M, and capture the successor relations using predicates; and from ϕ we encode the subformulas used in the labeling algorithm and capture their syntactic type again by using predicates.
For our case study, we encode the nodes of the Kripke structures and the automata of M as integers, and thus the nodes of GM as tuples of integers. The generated predicates use this encoding. As an example, the predicate encoding the labeling of GM vertices with formulas is defined as follows: bool Label(Formula f, GVertex u) (
(u.w=0 & Lab1(f,u.s0) ) | (u.w=1 & Lab2(f,u.s1) ) | (u.w=2 & Lab3(f,u.s2) ) | (u.w=3 & Lab4(f,u.s3) ) ) where Lab1, Lab2, Lab3, and Lab4 are the predicates capturing the labeling of the four Kripke structures of M , w is the u component denoting the current Kripke structure (i.e, the current world), and s0, s1, s2, and s3 denote the u components corresponding to the states of the respective Kripke structures.
We then encode the seven subformulas of ϕ1 as integers in the interval [
Once, all the predicates are defined, the original model-checking question, that is, determining whether M, w |= ϕ, can be translated in the following clause:
( exists GVertex u. Lambda(true,0,u) ), which, in our case study, simply asks the backend solver to verify whether a vertex of GM exists where the input formula ϕ1 holds true. Thus, in the second module, called COMPOSE FIXED-POINT FORMULA, we just put together the predicates computed by the first module with the fixed-point algorithm given in Figure 1 and the above clause.
The last module just invokes the backend solver Mucke on the built formula and returns its outcome. Evaluation. To evaluate our prototype tool we have elaborated a benchmark by extending the given case study with the layout of the environment. A layout is given as a bi-dimensional grid where the refrigerator, the door, the lounge (the base position of the robot) and some obstacles are positioned. This benchmark is parameterized on the size of the grid, the number of instances and the positioning of the objects (refrigerator, door, lounge, and obstacles). This will allow us to evaluate the scalability of the approach by varying the parameters. However, to date, we have only exercised our tool on a simple scenario (2 × 2 grid) against the two different Ctlbdi formulas given above. The tool has performed quite well: it gives the right answer in a fraction of a second with BBD maximum size of 1134. We were unable to perform a systematic evaluation since most of the translations in our tool are still performed manually which prevents us to manage large benchmarks. As future work, we plan to complete the automatization of the modules of our tool and then perform a full evaluation over the described benchmark.