Using Strategic Logics to Reason about Agent Programs

1 Introduction

In this paper we report on our work on using strategic logics for reasoning about the ability of agents developed under the Belief-Desire-Intention (BDI) agent-oriented programming tradition [Bratman et al., 1988; Rao and Georgeff, 1992; Bordini et al., 2006], a popular paradigm for building multiagent systems. In particular, we aim at providing a verification framework that will allow us to reason about what a group of agents' can achieve with their available know-how capabilities under the BDI paradigm, which enables abstract plans to be combined and used in real-time under the principles of practical reasoning [Bratman et al., 1988].

While recent work (e.g., [Alechina et al., 2007; 2008; Dastani and Jamroga, 2010]) has tried to better bridge the gap between formal logic and practical programming, this was done by restricting the logic's models to those that satisfy the transition relations of agents' plans and without reasoning about what a group of agents could achieve if they had specific capabilities.

To achieve our objectives, we adapt ATLES, a version of ATL (Alternating-time Temporal Logic) [Alur et al., 2002] with Explicit Strategies [Walther et al., 2007]. In ATL, one is interested in checking formulas of the form 〈〈A〉〉ϕ expressing that the coalition team of agents A has a joint strategy for guaranteeing that the temporal property ϕ holds. ATLES [Walther et al., 2007] extends ATL to accommodate formulas of the form 〈〈A〉〉ρϕ denoting that coalition A has a

∗The paper on which this extended abstract is based was the recipient of the best paper award of the 2012 European Conference on Logics in Artificial Intelligence [Yadav and Sardina, 2012] We acknowledge the support of the Australian Research Council (DP1094627 & DP120100332).

Sebastian Sardina

RMIT University Melbourne, Australia sebastian.sardina@rmit.edu.au

joint strategy for ensuring ϕ, when some agents are committed to specific strategies, as specified by so-called commitment function ρ. Here we go further and develop a logiccalled BDI-ATLES-in which commitments can be tied directly to the know-how of agents under the notion of practical reasoning embodied by the BDI paradigm [Bratman et al., 1988; Rao and Georgeff, 1992]: the only strategies that can be employed by a BDI agent are those that ensue by the (rational) execution of its predefined plans, given its goals and beliefs. 1 To achieve this, our framework includes a construct 〈〈A〉〉ω,ϱϕ stating that coalition A has a joint strategy for ensuring ϕ, under the assumptions that some agents in the system are BDI-style agents with capabilities and goals as specified by assignments ω and ϱ, respectively. For instance, a formula like 〈〈A〉〉∅,∅ϕ ⊃ 〈〈A〉〉ω,ϱϕ can be used to check if coalition A has enough know-how and motivations to carry out a task ϕ that is indeed physically feasible for the coalition.

2 Preliminaries

2.1 ATL/ATLES Logics of Coalitions

Alternating-time Temporal Logic (ATL) [Alur et al., 2002] is a logic for reasoning about the ability of agent coalitions in multi-agent game structures. ATL formulae are built by combining propositional formulas, the usual temporal operators-namely, © ("in the next state"), 2 ("always"), 3 ("eventually"), and U ("strict until")-and a coalition path quantifier 〈〈A〉〉 taking a set of agents A as parameter. As in CTL, which ATL extends, temporal operators and path quantifiers are required to alternate. Intuitively, an ATL formula 〈〈A〉〉φ, where A is a set of agents, holds in an ATL structure if by suitably choosing their moves, the agents in A can force φ true, no matter how other agents happen to move. The semantics of ATL is defined in so-called concurrent game structures where, at each point, all agents simultaneously choose their moves from a finite set, and the next state deterministically depends on such choices. More concretely, an ATL structure is a tuple M = 〈A, Q, P, Act, d, V, σ〉, where A = {1, . . . , k} is a finite set of agents, Q is the finite set of states, P is the finite set of propositions, Act is the set of all domain actions, d : A×Q ↦→ 2Act indicates all available actions for an agent in a state, V : Q ↦→ 2P is the valuation function stating what is true in each state, and σ : Q×Act|A| ↦→ Q is the transition function mapping a state q and a joint-move ⃗a ∈ D(q)-where D(q) = ×|A| i=1d(i, q) is the set of legal joint-moves in q -to the resulting next state q′ .

1 The notion of "rationality" used here is that found in the literature on BDI agent programming (as reasonable constraints on how the various mental modalities may interact), rather than that common in game-theory (generally captured via solution concepts).

To provide semantics to formulas 〈〈·〉〉ϕ, ATL relies on the notion of agent strategies. Technically, an ATL strategy for an agent agt is a function fagt : Q+ ↦→ Act, where fagt(λq) ∈ d(agt, q) for all λq ∈ Q+, stating a particular action choice of agent agt at path λq. A collective strategy for group of agents A ⊆ A is a set of strategies FA = {fagt | agt ∈ A} providing one specific strategy for each agent agt ∈ A. For a collective strategy FA and an initial state q, it is not difficult to define the set out(q, FA) of all possible outcomes of FA starting at state q as the set of all computation paths that may ensue when the agents in A behave as prescribed by FA, and the remaining agents follow any arbitrary strategy [Alur et al., 2002; Walther et al., 2007]. The semantics for the coalition modality is then defined as follows (here φ is a path formula, that is, it is preceded by©, 2, or U, andM, λ |= φ is defined in the usual way [Alur et al., 2002]):

M, q |= 〈〈A〉〉φ iff there is a collective strategy FA such that for all computations λ ∈ out(q, FA), we have M, λ |= φ.

The coalition modality only allows for implicit (existential) quantification over strategies. In some contexts, though, it is important to refer to strategies explicitly in the language, e.g., can a player win the game if the opponent plays a specified strategy? To address this limitation, Walther et al. [Walther et al., 2007] proposed ATLES, an extension of ATL where the coalition modality is extended to 〈〈A〉〉ρ, where ρ is a commitment function, that is, a partial function mapping agents to so-called strategy terms. Formula 〈〈A〉〉ρφ thus means that "while the agents in the domain of ρ act according to their commitments, the coalition A can cooperate to ensure φ as an outcome."

The motivation for our work stems from the fact that ATLES is agnostic on the source of the strategic terms: all meaningful strategies have already been identified. In the context of multi-agent systems, it may not be an easy task to identify those strategies compatible with the agents' behaviors, as those systems are generally built using programming frameworks [Bordini et al., 2006] that are very different from ATL(ES).

2.2 BDI Programming

The BDI agent-oriented programming paradigm is a popular and successful approach for building agent systems, with roots in philosophical work on rational action [Bratman et al., 1988] and a plethora of programming systems available, such as JACK, JASON, JADEX, 2APL [Bordini et al., 2006], and GOAL [de Boer et al., 2007], among others.

A typical BDI agent continually tries to achieve its goals (or desires) by selecting an adequate plan from its plan library given its current beliefs, and placing it into the intention base for execution. The agent's plan library Π encodes the standard operational knowledge of the domain by means of a set of plan-rules (or "recipes") of the form φ[α]ψ: plan

α is a reasonable plan to adopt for achieving ψ when (context) condition φ is believed true. For example, walking towards location x from y is a reasonable strategy, if there is a short distance between x and y (and the agent wants to be eventually at location x). Conditions φ and ψ are (propositional) formulas talking about the current and goal states, respectively. Though different BDI languages offer different constructs for crafting plans, most allow for sequences of domain actions that are meant to be directly executed in the world (e.g., lifting an aircraft's flaps), and the posting of (intermediate) sub-goals !ϕ (e.g., obtain landing permission) to be resolved. The intention base, in turn, contains the current, partially executed, plans that the agent has already committed to for achieving certain goals. Current intentions being executed provide a screen of admissibility for attention focus [Bratman et al., 1988].

Though we do not present it here for lack of space, most BDI-style programming languages come with a clear singlestep semantics basically realizing [Rao and Georgeff, 1992]'s execution model in which (rational) behavior arises due to the execution of plans from the agent's plan library so as to achieve certain goals relative to the agent's beliefs.

3 BDI-ATLES: ATL for BDI Agents

The overarching aim of this section is to allow the encoding of BDI applications in ATL in a principled manner. In particular, we imagine a BDI developer interested in what agents can achieve given their goals and capabilities. Hence, we envision BDI agents defined with a set of goals and so-called capabilities [Busetta et al., 1999; Padgham and Lambrix, 2005]. Generally speaking, a capability is a set/module of procedural knowledge (i.e., plans) for some functional requirement. An agent may have, for instance, the Navigate capability encoding all plans for navigating an environment. Equipped with a set of capabilities, a BDI agent executes actions as per plans available so as to achieve her goals, e.g., exploring the environment.

In this work, we shall consider plans consisting of single actions, that is, given BDI plan for the form φ[α]ψ, the body of the plan α consists of one primitive action. Such plans are akin to those in the GOAL agent programming language [de Boer et al., 2007], as well as universal-plans [Schoppers, 1987], and reactive control modules [Baral and Son, 1998]. Let ΠPAct be the (infinite) set of all possible plan-rules given a set of actions Act and a set of domain propositions P.

3.1 BDI-ATLES Syntax

The language of BDI-ATLES is defined over a finite set of atomic propositions P, a finite set of agents A, and a finite set of capability terms C available in the BDI application of concern. Intuitively, a capability term c ∈ C (e.g., Navigate) represents a plan library Πc (e.g., ΠNavigate ). As usual, a coalition is a set A ⊆ A of agents. A capability assignment ω consists of a set of pairs of agents along with their corresponding capabilities of the form 〈agt : Cagt〉, where agt ∈ A and Cagt ⊆ C. A goal assignment ϱ defines the goal base (i.e., set of propositional formulas) for some agents. It consists of set of tuples of the form 〈agt : Gagt〉, where agt ∈ A and Gagt is a set of boolean formulas over P. Aω denotes the set of agents whose capabilities are defined by assignment ω, i.e., Aω ={agt | 〈agt : Cagt〉 ∈ ω}. Set Aϱ is defined analogously.

The set of BDI-ATLES formulas is then exactly like that of ATL(ES), except that coalition formulas are now of the form 〈〈A〉〉ω,ϱϕ, where ϕ is a path formula (i.e., it is preceded by©, 2, or U), A is a coalition, and ω and ϱ range over capability and goal assignments, respectively, such that Aω = Aϱ. The intended meaning is as follows:

〈〈A〉〉ω,ϱϕ expresses that coalition of agents A can jointly force temporal condition ϕ to hold when BDI agents in Aω (or Aϱ) are equipped with capabilities as per ω and (initial) goals are as per ϱ.

Note that we require, in each coalition (sub)formula, that the agents for which capabilities and goals are assigned to be the same. This enforces the constraint that BDI-style agents have both plans and goals. So, a formula of the form 〈〈A〉〉∅,{〈a1:{γ}〉}ϕ is invalid, as agent a1 has one goal (namely, to bring about γ), but its set of plans is undefinedwe cannot specify what its rational behavior will be. ndition for player Ag is ψWIN= GB ∧ AgB : the player wins when collocated with gold at the depot.

3.2 BDI-ATLES Semantics

A BDI-ATLES concurrent game structure is a tuple M= 〈A, Q, P, Act, d, V, σ, Θ〉, where:

• A, Q, P, Act, d, V and σ are as in ATL(ES).
• There is a distinguished dummy action NOOP ∈ Act such that NOOP ∈ dagt(q) and σ(q, 〈NOOP, . . . , NOOP〉) = q, for all agt ∈ A and q ∈ Q, i.e., NOOP is always available to all agents and the system remains still when all agents perform it.
• Capability function Θ : C ↦→ F(ΠPAct ) maps capability terms to their (finite) set of plans. (Here, F(X) denotes the set of all finite subsets X.)

BDI-ATLES models are similar to ATLES ones, except that we use capability terms instead of strategy terms. In a nutshell, the challenge thus is to characterize what are the underlying "low-level" ATL strategies for agents with certain capabilities and goals. We call such strategies rational strategies, in that they are compatible with the standard BDI rational execution model [Rao and Georgeff, 1992]: they represent the agent acting as per her available plans in order to achieve her goals in the context of her beliefs.

So, given an agent agt ∈ A, a plan-library Π, and a goal base G, we define Σagt Π,G as the set of standard ATL strategies for agent agt inM that are rational strategies when the agent is equipped with plan-library Π and has G as (initial) goals. These ATL strategies are such that the agent always chooses an action that is compatible with its available plans in order to achieve one of its goals in the context of its current beliefs. The intuition behind defining set Σagt Π,G is to identify those "rational traces" in the structure that are compatible with the BDI deliberation process in accordance with the agent's goals and beliefs. Rational strategies, then, are those that only yield rational traces, which are in turn defined in three steps:

1. First, we define a goal-marking function g(λ+, i) denoting the "active" goal base of the agent at the i-th stage of trace λ+.
2. Second, we define the set of indexes (i.e., stages) Exec(φ[α]ψ, g, λ+) in trace λ+ where the plan φ[α]ψ may have been executed by the agent: the plan's precondition φ was true, ψ was an active goal of the agent (as directed by goal-marking function g), and α was indeed performed.
3. Third, we define a rational trace λ+ as one in which the agent has always executed one of its plans: for every index i, it is the case that i ∈ Execagt(φ[α]ψ, g, λ+), for some plan φ[α]ψ in her know-how library.

Finally, we use Σagt Π,G to denote the set of all ATL strategies whose executions always yield rational traces. The technical details of all the above steps and notions can be found in [Yadav and Sardina, 2012].

With the set of rational strategies Σagt Π,G suitably defined, we are ready to detail the semantics for formulas of the form 〈〈A〉〉ω,ϱϕ. Following ATLES, we first extend the notion of a joint strategy for a coalition to that of joint strategy under a given capability and goal assignment. So, given a capability (goal) assignment ω (ϱ) and an agent agt ∈ Aω (agt ∈ Aϱ), we denote agt's capabilities (goals) under ω (ϱ) by ω[agt] (ϱ[agt]). Intuitively, an 〈ω, ϱ〉-strategy for coalition A is a joint strategy for A such that (i) agents in A ∩ Aω only follow "rational" (plan-goal compatible) strategies as per their ω-capabilities and ϱ-goals; and (b) agents in A\Aω follow arbitrary strategies. Formally, an 〈ω, ϱ〉-strategy for coalition A (with Aω = Aϱ) is a collective strategy FA for agents A such that for all fagt ∈ FA with agt ∈ A∩Aω, it is the case that fagt ∈ Σagt Π,G , where Π = ∪c∈ω[agt]Θ(c) and G = ϱ[agt]. Note no requirements are asked on the strategies for the remaining agents A\Aω, besides of course being legal (ATL) strategies.

Using the notions of 〈ω, ϱ〉-strategies and that of possible outcomes for a given collective strategy from ATL (refer to function out(·, ·) from Preliminaries), we are now able to state the meaning of BDI-ATLES (coalition) formulas: 2

M, q |= 〈〈A〉〉ω,ϱϕ iff there is a 〈ω, ϱ〉-strategy FA such that for all 〈ω, ϱ〉-strategies FAω\A for Aω \ A, it is the case that M, λ |= ϕ, for all paths λ ∈ out(q, FA ∪ FAω\A).

Intuitively, FA stands for the collective strategy of agents A guaranteeing the satisfaction of formula ϕ. Since FA is a 〈ω, ϱ〉-strategy, some agents in A-those whose capabilities and goals are defined by ω and ϱ, resp.-are to follow rational strategies. At the same time, because other agents outside the coalition could have also been assigned capabilities and goals, the chosen collective strategy FA needs to work no matter how such agents (namely, agents Aω \ A) behave, as long as they do it rationally given their capability and goal assignments. That is, FA has to work with any rational collective strategy FAω\A. Finally, the behavior of all remaining agents-namely those in A \ (A ∪ Aω)-are taken into account when considering all possible outcomes, after all strategies for agents in A ∪ Aω have been settled.

2 As with ATL(ES), ϕ ought to be a path formula and is interpreted in the usual manner. We omit the other ATL-like cases for brevity; see [Walther et al., 2007].

4 BDI-ATLESModel Checking

In order to model checking a formula 〈〈A〉〉ω,ϱϕ against a BDI-ATLES model M, one has to consider the rational choices of each BDI agent. These rational choices are the consequence of the agent's goals and capabilities specified by functions ϱ and ω in formula. The core idea, then, is to restrict the options of the BDI agents at each step relative to their applicable plans. Next, we extend the model M to embed the possible goals (based on the goal assignment) of BDI agents into each state, then we discuss the model checking algorithm and its complexity.

Given a BDI-ATLES model M=〈A, Q, P, Act, d, V, σ, Θ〉 and a goal assignment ϱ, the goal-extended model is a tuple Mϱ=〈A, Qϱ, P, Act, dϱ, Vϱ, σϱ, Θ〉, where:

• Qϱ ⊆ Q× ∏agt∈Aϱ 2ϱ[agt] is the set of extended states, now accounting for the possible goals of BDI agents. When qϱ = 〈q, g1, . . . , g|Aϱ|〉 ∈ Qϱ, where q ∈ Q and gi ⊆ ϱ[agti ], is an extended state, we use ws(qϱ) = q and gl(agti , qϱ) = gi to project M's world state and agti 's goals. To enforce belief-goal consistency we require no agent ever wants something already true: there are no qϱ ∈ Qϱ, agt ∈ Aϱ, and formula γ such that V(ws(qϱ)) |= γ and γ ∈ gl(agt, qϱ).
• Vϱ(qϱ) = V(ws(qϱ)) and dϱ(agt, qϱ) = d(agt, ws(qϱ)), for all qϱ ∈ Qϱ, that is, state evaluation and physical executability remains unchanged.
• σϱ(qϱ,⃗a) = 〈q′ , g′1 , . . . , g′ |Aϱ| 〉, where q′ = σ(ws(qϱ),⃗a) and g′i = gl(agti , qϱ) \ {γ | γ ∈ gl(agti , qϱ), V(q′ ) |= γ}, is the transition function.

States of model Mϱ are similar to that of M, except that they also include possible agent's goals. Observe that the transition relation caters for persistence of goals as well as dropping of achieved goals. Hence, the transition relation is well-defined within Qϱ states. Interestingly, though, the extended model ensures rationality with respect to goals is maintained, it does not restrict the original physical executability of actions. Therefore, the extended model accommodates both rational and irrational paths. However, it is now possible to distinguish between them, as one can reason about applicable plans in each extended state.

As standard, [ϕ]M denotes the set of states in M satisfying the formula ϕ. We extend ws(·) projection function to sets of extended states, that is, ws(S) = ⋃q∈S {ws(q)}. Thus, ws([ϕ]Mϱ ) denotes the set of all world states in M that are part of an extended state in Mϱ satisfying the formula ϕ. Also, JϱK denotes the set of extended states where the agents' goals are as per goal assignment ϱ; formally, JϱK = {q | q ∈ Qϱ, ∀agt ∈ Aϱ : gl(agt, q) = ϱ[agt]}.

Figure 1 shows the model checking algorithm for BDI-ATLES. It is based on the symbolic model checking algorithm for ATL [Alur et al., 2002] and ATLES [Walther et al., 2007]. The first three cases are handled in the same way as in ATL(ES). To check the BDI-ATLES coalition formulae 〈〈A〉〉ω,ϱϕ, we extend the model as above (relative to the formula's goal assignment ϱ), and then check the plain ATL coalition formula 〈〈A〉〉ϕ in such extended model. Note that only the set of states having the goals as per the initial goal assignment are returned- initial goals of all agents are active in the first state of any rational trace. Unlike standard ATL model checking, we restrict the agents' action choices as per their capabilities. We do this by modifying the usual pre-image function Pre(·) to only take into account actions compatible with agents' applicable plans. Intuitively, Pre(A, ω,Θ, ρ) is the set of (extended) states from where agents in coalition A can jointly force the next (extended) state to be in set ρ no matter how all other agents (i.e., agents in A \ A) may act and provided all BDI-style agents (i.e., agents with capabilities defined under ω and Θ) behave rationally. Due to lack of space we omit the formal definition of Pre, which can be found in [Yadav and Sardina, 2012].

It is easy to see that the extended model is, in general, exponentially larger than the original one with respect to the number of goals maxagt∈A(|ϱ[agt]|) and agents |Aϱ|. A more promising case arises when goals are given a reactive maintenance interpretation [Duff et al., 2006; Dastani et al., 2006]-conditions that ought to be restored whenever "violated". Interestingly, under such interpretation of goals, we retain ATL(ES) polynomial complexity, which is of course a tight bound as the resulting framework subsumes ATL (just take ω = ϕ = ∅) and model checking ATL is PTIMEcomplete [Alur et al., 2002]. See [Yadav and Sardina, 2012] for details.

5 Conclusion

We have proposed a framework for verifying BDI-type agents using an ATL-like logic, thus bringing together work in verification of strategic behaviour and agent programming.

Among other things, we would like to extend our work to more general agent programs as well as to investigate how to integrate plausibility reasoning [Jamroga and Bulling, 2007] in our logic to focus the verification to certain parts of an ATL structure using more declarative specifications.