Dynamic verification of hierarchical multi-agent plans

Abstract

Planning agents evolving in dynamic and complex environments need to continually plan their tasks and to monitor the evolution of its execution in order to deal with unexpected situations. To face this challenge, we proposed, in previous works, HPINet (Hierarchical-Task-Petri-Net) and SHPINet (HPINet with synchronization), models that can be used to represent plans less sensitive to execution contexts, and that support automatic verification. In this paper, we aim to propose computational techniques to verify some keys properties, such as soundness, of executing partial plans by analyzing their abstract level of representation. We especially focus on the some theorems and their corresponding proofs about the soundness of plan.

Keywords

Multi-agent plan verification Petri net plans analysis automating planning planning and execution interleaving

1. Introduction

In this paper, we are interested in the continual multi-agent planning and coordination where the planning, coordination and execution processes have to be interleaved and carried out in continual fashion in order to solve complex tasks in unpredictable and dynamic environments. These environments could be subject to occurrence of unexpected events related to the failure of actions, the failure of required resources, the fault in execution platform, or the errors of the designer or programmer. The occurrence of unexpected events during plans execution can alter the conditions under which these plans are generated and coordinated, which can lead to their failure. On the other hand, the execution of plans in dynamic environments might provide opportunities for the agents to accomplish their goals more efficiently or effectively [9]. In this context, to protect plans from adverse effects and to profit from the new opportunity, interacting agents have to continue planning and coordination during plans execution in order to adjust their planned tasks with new contexts. To have this capability, the agents must be able to continually verify the soundness of their plans, monitor the evolution of their execution and environment, and better switch between local planning, coordination, and execution.

Whatever the continual planning and coordination approach is attractive to cope with complex and dynamic environments issues, it faces a key challenge related to the higher computational and communication cost that compromise the agents to react adequately to eventual exceptions (which is not preferable in highly dynamic environment) [7]. Computation complexity refers firstly to the monitoring of environment and execution evolution, and secondly to the local plans refinement, adaptation and repairing. However, communication complexity refers to the coordination of local adjustments to manage commitments with each other [5].

To deal with this challenge, we provided in previous works [2, 3], a formalism called SHPlNet (Hierarchical-Task-Petri-Net with synchronization) that allows to represent hierarchical plans (that is used by most preferred continual planning techniques [9]) with multiple abstraction levels, by extending the Petri net (as in [15]) and by taking advantage of HTN (Hierarchical Tasks Network) planning [10, 11], CHiP [6], and the modular analysis of Petri nets idea [4]. Overall, the SHPlNet formalism is featured with the following characteristics that are very advocated by continual multi-agent planning. Firstly, it can take into account the representation of flexible plans with implicitly representing many execution alternatives. These one enable the plans to be less sensitive to the execution context and reducing dynamic adjustment complexity. Secondly, by using Petri net, the execution context is explicitly represented by the marking concept. In this fashion, SHPlNet formalism offers the necessary features that allow interacting agents to monitor plans evolution, to handle plans interaction and interdependency, and to control resources evolution at run time. By using so called summary information [6], the plans might be verified and adjusted by only analyzing its abstract level. Thirdly, SHPlNet formalism can enable modular representation of plans: there is a clear distinction between the abstraction levels of hierarchical plan, and also there is clear separation between tasks and synchronization constraints. Within this aspect, the analysis of plans can be done in a modular way, and therefore, their updating may be simplified. Note that the modular representation of the plan can facilitate the revision of some decisions of planning and coordination, and therefore best meet the evolutionary aspect of the system.

This paper aims to complement our previous work with a theoretical framework to use for dynamic verification and validation of agent and multi-agent plans, and to present how this framework is used by interaction agents to switch between planning/coordination and execution. We proceed to specify the conditions in which a partial plan (partially refined and executed) represented by SHPlNet will be accomplished in some way, will be accomplished in any way, or will not be accomplished in any way, these all by analyzing only the representation of their abstract level. We call respectively these properties feasibility, soundness, and invalidity. We provide also the underlying computational techniques to verify and validate these properties. We especially focus on the some lemmas, theorems, and their corresponding proofs about the soundness of plans represented by a SHPINet. Indeed, we present some algorithms for computing and updating summary information, which is the basis of abstract reasoning on plans.

The rest of this paper is structured as follows. In Section 2, we provide an overview on the paper context and the assumptions this work is based on. We outline also the intuition behind the model used to represent plans and the key properties related to. To master the complexity of the work, we follow a progressive approach. Throughout the paper, we specify the conditions that must be hold for a partial plan represented by SHPlNet to be feasible, sound, or invalid. We insist on proposing a verification technique that exploits as much as possible the high abstraction levels of the hierarchical plans and limits the use of the accessible graph. As the formalism of SHPlNet is incrementally formed from simple feathers (as it will be presented throughout paper sections), from HTPN to HPlNet1 to SHPlNet, the conditions to be hold for each property will also be built progressively according to. In Section 3, we specify the conditions to verify in order to decide whether the execution of a plan represented as HTPN is feasible, sound, or invalid. For this end, we proceed to make the first abstraction of SHPlNet representation by ignoring the Summary information and Synchronization constraints. In this level we are only focused on the control flow between tasks and the impact of organizational structure of tasks on their accomplishment. In Section 4, we present HPlNet and outline the impact of resources constraints related to the tasks in plans on feasibility, soundness, and invalidity properties verification process. We clear in this section the reachability graph analysis based verification and the summary information based verification. Section 5 focuses on tasks synchronization and how to verify the plans represented by SHPlNet by considering this synchronization. We extend the conditions so that the plans represented by SHPlNet are feasible, sound, or invalid according to the corresponding conditions in the case of HPLNet. Section 6 outlines relevant related works. Finally, we conclude our paper.

2. Background and overview

We advocate an approach where a team of deliberative agents has to continually elaborate and execute a set of concurrent partial plans in order to accomplish a set of goals. As tasks in local or global plan may be interrelated due to the functional relationships or due to the sharing of common resources required for its accomplishment, agents’ plans must be coordinated in order to avoid harmful situations and to benefit from the synergy of their tasks.

In order to ensure a safe behavior during plans execution in the entire system, plans of all agents must be benefic and conflict free. The verification of plans validity must be accomplished before its execution is started and while they are being executed.

In this section, we provide an overview on the paper context and the assumptions this work is based on. We outline also the intuition behind the model used to represent plans and the key properties to be verified.

2.1 Partial hierarchical plan

In this paper we are based on hierarchical plans where a set of tasks are organized in tree-like structure. The top level includes the root of the tree that is the abstract (compound) task and the lowest level includes the leaves that are elementary (ground, or primitive) tasks, which may be accomplished directly by execution of actions. Several decomposition methods may be related to an abstract (sub) task. The middle levels include less abstract subtasks and decomposition methods. The hierarchical representation is a natural approach for representing practical activities and goals. It gives also a clear idea on how the accomplishing of complex tasks may be simplified.

Figure 1.

Decomposition of the manufacturing task.

Figure 1 shows an example of hierarchical plan describing the decomposition of a complex task, noted Build-P&Q, for building two kings of parts P and Q by automatic manufacturing unit. This plan illustrates how each task can be decomposed (resp. instantiated) to others tasks in the next level. Hence, Build-P&Q can be decomposed into two parallel (independent) tasks Build-P (construct the part P) and Build-Q (construct the part Q). These tasks are linked to Build-P&Q by AND operator. Build-P is decomposed into two sequential tasks Prepare-q and Build-P-from-q. This means that the part P has to be built in two steps: prepare a part q in first step and use q to build P in second step. In his tours, Prepare-q can be decomposed according to two alternative decomposition methods: Produce-q-from-scratch (for producing the part q from feedstuff) and Obtain-q-from-O (for detaching the part q from the part O). These tasks (may be considered as decomposition methods) are linked to Build-P by OR operator. The manufacturing of Q is accomplished in three sequential steps: produce the parts H and L, transport these parts to the room Rm, and finally build Q from H and L. The manufacturing of the different parts is accomplished in two units by using two machines M1 and M2 and a tool tl. To move parts, it is possible to use a transportation of a type tp. The tool tl is used by the task Disassemble-O.

We note that hierarchical plans represented in this way are considered as partial plans because the order of execution between parallel tasks and the choice of decomposition methods for decomposing abstract tasks are not entirely specified. Therefore, one hierarchical plan can be refined to a set of total ordered ground (executable) plans. In the latter case, the plan is said to be flexible.

2.2 SHPlNet

In this subsection, we present an overview of the formalism, that we called SHPlNet (Hierarchical-Plan-Net with Synchronization), proposed to represent hierarchical plans with synchronization. The foundation of this formalism is based on three concepts, hierarchy, abstraction, and synchronization. These concepts are featured in two components: Hierarchical-Plan-Net (HPlNet) and synchronization net (S). Graphically, HPlNet and S are separated by a vertical line, HPlNet component is upper the line and S component is under the line. Figure 2 shows an instance of SHPlNet in which HPlNet component represents the hierarchical task tree of Fig. 1.

Figure 2.

Graphical representation of an SHPlNet instance.

The keys properties of the formalism SHPlNet can be summarized in four points:

•

Hierarchical tasks representation, where we distinguished between abstract and elementary transitions to be able to represent the tasks in different levels of abstraction. In Fig. 2 Build-P&Q, Build-P, Build-Q, Produce-H&L, Prepare-q are abstract transitions (or abstract tasks) and Move-H&L-to-Rm, Build-Q-from-H&L, Build-P-from-q, Produce-L, Produce -H, Produce-q, Disassemble-O, Move-q-to-Rm are elementary transition (or elementary tasks). Each abstract task in one level is connected to one or more macro-nodes or Task-Petri-Nets, $n_{1}$ , $n_{2}$ , …, $n_{6}$ in Fig. 2, of a lower level by refinement rules, $r_{1}$ , $r_{2}$ , $r_{3}$ , $r_{4}$ , $r_{5}$ , $r_{6}$ in the same figure.

•

Summary information computing and using, where we proceed to associate supplementary information to transitions, using a function $R e s$ , to represent explicitly the link between the tasks and resources to consume and to produce by these tasks. In Fig. 2, the task Produce-q has to consume (resp. to produce), as is specified by the designer, 2 units of $f d$ and 1 unit of $M_{1}$ (resp. 1 unit of $q$ and 1 unit of $M_{1}$ ). Hence, $Res(\verb"Produce-q")=\langle\{(fd,2),(M_{1},1)\},\{q,1),(M_{1},1)\}\rangle$ . The resources to consume (resp. to produce) of the task Prepare-q are computed from lowest-level tasks and represented in terms of lower and upper values. If we do not consider synchronization net, $Res(\verb"Prepare-q")=\langle\{(fd,0,2),(M_{1},0,1),(tl,0,1),(O,0,1),(tp,0,1)% \},\{(q,1,1),(q^{\prime},0,2),$ $(M_{1},0,1),$ $(tl,0,1),(tp,0,1)\}\rangle$ . Summary information enable also to reason (e.g. identify and analyze positive and negative interaction’ situations of tasks) on abstract and partial plans without analyzing their entire lowest levels.

•

Explicit separation between tasks and synchronization constraints. The Petri net S in Fig. 2 represents a constraint that enforce a sequential execution of concurrent tasks (transitions) Produce-L and Produce-H, a constraint that enforce an exchange of 1 units of $M_{1}$ between Produce-H (producer) and Produce-q (consumer), and a constraint to prevent the selection of the refinement rule $r_{6}$ . This aspect can facilitate the analysis of plans and the revision of some decisions (represented by synchronization net) by planning and coordination process in order to best meet continual planning requirements.

•

Explicit execution state representation, where we exploit the marking concept to provide an explicit representation of plans execution states. This can enable agents to dynamically reason on the evolution of plans.

The representation of hierarchical tasks, which we call HTPN (Hierarchical-Task-Petri-Net), is considered as an abstraction of HPlNet by ignoring the Summary information. On other hand, HPlNet is considered as an abstraction of SHPlNet by ignoring the Synchronization constraints.

2.3 Verification of plans

In this paper, we are interested in the verification of plans’ validity before and during their execution. On the basis of verification result, interacting agents might take appropriate decisions. During their elaboration, the plans must be verified to ensure that are valid and conflict free. During their execution, they must be verified to ensure that the outcome of executed actions is as expected during planning and required conditions for continuing the remained actions yet satisfied.

Definition of plan verification technique depends on the semantic that one can associate to plan execution. In this paper we are based on operational semantics to describe the plans’ execution and its interfering with its execution context. The execution is hence described in terms of sequence of successive (execution) states. Initial state is that where no action of the plans has been executed and final state is the state where the plan is fully executed. Steps between states refer to the execution of actions (elementary tasks) or the selection of decomposition methods for abstract tasks. So, verification process try to decide whether the execution of plan leads always, sometime (under certain conditions), or never to a safe final state. These properties are summarized as follows:

•
Soundness: Soundness property denotes that the plan execution will never reach blocking state. The only sink state must be the final state. Therefore, a plan is said to be sound if and only if its execution is always properly terminated. In the same vein, a partial plan is called sound if its execution leads always to final state whatever the choices to make for its refinement. Soundness property denotes also the absence of conflict between actions or tasks and all required resources are sufficiently available.
•
Feasibility: A plan is feasible if it can be executed correctly. In other words, this property denotes that the plan execution can reach a final state if best choices are made. In the same vein, a partial plan is said to be feasible if the ability of its execution to reach to final state depends to the choices to make for its refinement. In a multi-agent context, this property may also mean that execution of individual plans can succeed if they agree to make some minor arrangements.
•
Invalidity: This property denotes that the execution of plan can never reach a final state. A plan is said to be invalid if it cannot in any way be executed correctly. In the same vein, a partial plan is called invalid if its execution cannot lead the final state whatever the choices that can be made. This plan is therefore conflicting and its repairing requires questioning certain planning and coordination decisions.

Figure 3.
The use of feasibility, invalidity, and soundness properties in planning/execution phases.

The agents in the system try to verify these properties in order to behave in an appropriate manner and to take suitable decisions. Figure 3 illustrates how these properties are verified through the planning/execution phases. Before the execution is started, the plan must be progressively refined by reorganizing its tasks and by selecting a refinement rules for decomposition of abstract tasks. The progress of plan elaboration will continue as long as possible. If the planning/coordination process reaches a state where the plan is invalid it will backtrack in order to examine other planning alternative. A plan passes to execution phase if it is sound and will return to planning/coordination phase if it will be invalid (because it will not success to reach goal state). When a plan is being executed its verification go on. If its state is yet sound then the execution can be go on. However, if the state becomes feasible (resp. invalid) the plan must be adapted (resp. suspended). The adaptation of plan consists of blocks the choices that can lead to unsafe states and imposes synchronization constraints between concurrent tasks.

Throughout the paper, we specify the conditions that must be hold for a partial plan represented by SHPlNet to be feasible, sound, or invalid. We insist on proposing a verification technique that exploits as much as possible the high abstraction levels of the hierarchical plans and limits the use of the accessible graph. As the formalism of SHPlNet is incrementally formed from simple feathers (as it will be presented throughout paper sections), from HTPN (Hierarchical Task Petri Net) to HPlNet (Hierarchical Plan Net) to SHPlNet, the conditions to be hold for each property will also be built progressively according to.
2.4 Dealing with team of agents

In the previous section, we present the key properties that have to verify during planning/coordination and execution phases. If the verification of local plans is easy, the verification of multi-agents plan is difficult, firstly, due to the absence of global vision on all agents’ plans. Second difficulty concerns the private nature of these plans, when the agents are self-interested, the information must remain private. In this paper, we are not interested in the distributed algorithm to use for verifying multi-agents plan. We especially deal with centralized technique for analyze local or multi-agent plans. The centralized analysis is used in many planning approach even if coordination is not totally centralized. In [16, 1, 8] for example the agent that want elaborate or validate its plan in multi-agent context, forms a global plan by merging its local plans with those of all others agents. To allow an agent to have a (partial) global view, it must exchange with others agents its plan or only information on its plan.

In the system where the agents are self-interested and when information on plans must remain private, these agents do not communicate their plans with each other. In this paper, we cope with this issue by presenting a verification technique that allows an agent to analyze abstract level of hierarchical plans without having to analyze their entirety detail. The technique to propose is not based on the analysis of the entire reachability graph. However, it is based on the summary information associated with abstract tasks. Hence, the detailed plans are only exchanged with tightly coupled agents.

3. Simple hierarchical tasks

In this section, we start with, HTPN (Hierarchical-Task-Petri-Net), the first abstraction of SHPlNet by ignoring the summary information and the synchronization constraints. We present how to formalize the representation of hierarchical task networks based on Petri net. We are focused on the control flow between tasks, how abstract tasks can be decomposed, and the representation of their evolution states. The key idea consists of defining a tree-based structure of macro-nodes. Each macro-node is tasks network that implement decomposition method for abstract task. Through this section; we explain how to verify the key property argued in the Section 2.3.

3.1 Tasks network

We start by explain how we use Petri net to represent a tasks network. We adopt two patterns of control flow, one to represent parallel (or partially ordered) tasks and the other to represent the sequential (or totally ordered) tasks. Secondly, we use a special end-transition. We called the resulting formalism Task Petri net (or TaskPN). Figure 4 illustrates two instances of TaskPN: Sequential-TaskPN (Fig. 4a), and Parallel-TaskPN (Fig. 4b).

Figure 4.

Examples of (a) Sequential-TaskPN, and (b) Parallel-TaskPN.

Formally, we define Task Petri Net (TaskPN) as follows (Definition 1):

.

Task Petri NetWe define a Task Petri Net (TaskPN) by the tuple $(P,T,F,W,s,e)$ where: $(P,T,F,W)$ is a Petri net; and:

•

$s$ is a particular place representing the source place $(\bullet s=\emptyset)$ ; $e$ is a particular transition representing the end transition $(e\bullet=\emptyset)$ .

•

$W:F\rightarrow{1}$ .

•

$(P,T,F,W)$ has either of the following two structures:

–

All transitions and places belong to one single path from $s$ to $e$ ), i.e. $P=\{s\}\cup\bigcup_{i=1}^{m}{\{p_{i}\}}$ , $T=\bigcup_{i=1}^{m}{\{t_{i}\}}\cup\{e\}$ , and $F=\{(s,t_{1})\}\cup\bigcup_{i=1}^{m}{\{(t_{i},p_{i})\}}\cup\bigcup_{i=1}^{m}{% \{(p_{i},t_{i+1})\}}\cup\{(p_{m},e)\}$ . in this case, $(P,T,F,W,s,e)$ is called Sequential-TaskPN.

–

All (tasks) transitions belong to parallel paths from the fork-transition $f\in T$ (having the unique input place $s$ ) to the end-transition $e$ , i.e. $P=\bigcup_{i=1}^{n}{\{p_{i},p^{\prime}_{i}\}}\cup\{s\}$ , $T=\bigcup_{i=1}^{n}{\{t_{i}\}}\cup\{f,e\}$ , and $F={(s,f)}\cup\bigcup_{i=1}^{n}{\{(f,p_{i})\}}\cup\bigcup_{i=1}^{n}{\{(p_{i},t_% {i})\}}\cup\bigcup_{i=1}^{n}{\{(t_{i},p^{\prime}_{i})\}}\cup\bigcup_{i=1}^{n}{% \{(p^{\prime}_{i},e)\}}$ ; tasks are connected to source place by a fork transition $f$ . in this case, $(P,T,F,W,s,e)$ is called Parallel-TaskPN.

Places in TaskPN represent execution states. A task, $t$ , is ready to be executed (enabled) if its input places, $\bullet t$ , are marked. The initial execution state is formalized by initial marking where the source place is the only to be marked (by only one token), we note $M_{0}=s$ . However, in the final marking all places are empty or $M_{f}=0$ , the end-transition $e$ removes all tokens.

3.2 Hierarchical tasks: HTPN

To represent hierarchical tasks we firstly proceed to distinguish between abstract (compound) and elementary (ground) tasks representation. secondly, we proceed make mapping between abstract transitions (representing compound tasks) and Task-PN nodes to represent decomposition methods. Resulting formalism is called Hierarchical-TaskPN (HTPN) [2].

Figure 5.

An instance of HTPN for building the part P.

An instance of HTPN has tree-like structure. Each node in this tree is a TaskPN. Figure 5 illustrates an instance of HTPN representing the component task Build-P (described in Section 2.1). We formally define HTPN as follows:

.

Hierarchical Task Petri NetA Hierarchical Task Petri Net (HTPN) is defined by the tuple: $(P,T,F,W,s,e,R)$ where:

•

$(P,T,F,W,s,e)$ is a TaskPN,

•

$T=T_{elem}\cap T_{abs}$ is a finite set of transitions, disjoint union of elementary ( $T_{elem}$ ) and abstract transitions ( $T_{abs}$ ); $T_{abs}$ may be empty,

•

$R\subseteq T_{abs}\times HTPN$ is a finite set of refinement rules for all abstract transitions ( $T_{abs}=\emptyset\Leftrightarrow R=\emptyset$ ); each rules $r\in R$ associates to a transition $t\in T_{abs}$ a refinement HTPN. We write $R=\cup_{t\in T_{abs}}R_{t}$ such that $R_{t}$ denotes the set of all rules to use for refining the task $t$ .

A HTPN $\mathcal{P}=(P,T,F,W,s,e,R)$ is considered as a tree of nodes having TaskPN structure. The root of this tree is $(P,T,F,s,e)$ where $T_{abs}=\{t_{0}\}$ and $T=\{e,t_{0}\}$ , $t_{0}$ is highest-level task of $\mathcal{P}$ . The leaves of the tree are nodes where $R=\emptyset$ ( $T=T_{elem}$ ). The intermediate nodes are characterized by $R\neq\emptyset$ ( $T_{a}bs\neq\emptyset$ ).

A HTPN is used to represent a space of all tasks an agent or a team of agents may accomplish to reach a global system goal (represented by the highest-level task). We note that HTPN is proposed to emphasize only on the subtask and control flow relationship between tasks. HTPN allows also the agents to have explicit states (indicating enabled, executed, and executing tasks) and to reason on their tasks evolution. This is by the marking concept of places and transitions. To specify the execution evolution, we are focused on the operational semantic. The states are represented in terms of places and abstract transitions marking. Each place may be marked at most by one token and the abstract transition by one node selected to refine him. Steps between states denote execution of elementary transitions or selection of refinement rules. We describe respectively, by Definitions 3 and 4, the state of HTPN and the condition and rules for their execution.

.

State of HTPN

•

A state of a HTPN $\mathcal{P}$ is defined by tree $Tr=(N,n_{0})$ such that $N$ is the set of node; each node $n\in N$ is a tuple $(Pl,Mp,Mt)$ such that $P l$ is a node in $\mathcal{P}$ ; $Mp:P(Pl)\rightarrow{0,1}$ and $Mt:T_{abs}(Pl)\rightarrow N\cup\{\varepsilon\}$ ( $\varepsilon$ denotes the absence of tokens) are respectively marking functions of places and abstract transitions; $n_{0}\in N$ is the root of tree; a node $n^{\prime}$ is the child of $n$ in $T r$ if and only if $\exists t\in T_{abs}(Pl(n))$ such that $(t,Pl(n^{\prime}))\in R(Pl(n))$ , and $Mt(n)(t)=n^{\prime}$ .

•

The initial state $Tr_{0}=(\{n_{0}\},n_{0})$ . such that $n_{0}=(Pl,Mp_{0},Mt_{0})$ where $Mp_{0}=s(Pl(n_{0}))$ and $Mt_{0}=\varepsilon$ are the initial markings.

•

The final state $Tr_{f}$ is an empty tree (that has no node, noted $Tr_{f}=\bot$ ).

•

A marked HTPN of $\mathcal{P}$ is the tuple $(\mathcal{P},Tr_{0})$ .

The state of HTPN is considered as an extended marking that indicates the activated nodes and the marked place and (abstract) transitions in these nodes. The initial state is generated when the execution of the task, at the top level, $t_{0}$ , is launched for the first time. However, the final state is reached when this task is accomplished. Finally, each intermediate state specifies the current executing tasks, tasks that are finished and those that are not yet.

.

Execution condition and execution rules of HTPNLet $T r$ be a state, $n$ and $n^{\prime}$ be two nodes in $T r$ , and $s p$ be a step in $n$

•

$s p$ is enabled in $T r$ , denoted by $Tr\xrightarrow{sp}$ , iff: $(sp\in T(Pl(n))\Rightarrow(\forall p\in\bullet sp,Mp(n)(p)=1))$ and $(sp\in R_{t}\Rightarrow Tr\xrightarrow{t})$

•

the execution (or firing) of $s p$ in $T r$ leads to state $Tr^{\prime}$ , denoted by $Tr\xrightarrow{sp}Tr^{\prime}$ , such that:

–

$(sp\in T_{elem}(Pl(n)))\Rightarrow((N(Tr)=N(Tr^{\prime}))\wedge(Mp(n)% \xrightarrow{sp}Mp^{\prime}(n)))$

–

$(sp\in R_{t}(Pl(n)))\Rightarrow((Mp^{\prime}(n)=Mp(n)-W(Pl(n))(.,t))\wedge(N(% Tr^{\prime})=N(Tr)\cup\{n^{\prime}=(Pl,Mp_{0}(Pl),Mt_{0}(Pl))/r=(t,Pl)\})% \wedge(Mt^{\prime}(n)(t)=n^{\prime}))$ .

–

$(sp=e(Pl(n))$ and $n$ is child of $n^{\prime}$ by $r=(t^{\prime},Pl(n)))\Rightarrow((Mt^{\prime}(n^{\prime})(t^{\prime})=% \varepsilon)\wedge(N(Tr^{\prime})=N(Tr)-\{n\})\wedge(Mp^{\prime}(n^{\prime})=% Mp(n^{\prime})+W(Pl(n^{\prime}))(t^{\prime},.)))$

–

$(sp=e(Pl(n_{0}))\Rightarrow Tr^{\prime}=\bot$

One can note that the selection of a refinement rule leads to activation of a new node and the execution of end-transition to its deactivation. The execution of an abstract task is composed of a sequence of steps, starts by the selection of refining node and finishes by firing the end-transition of this node. Note that if an abstract task (transition) is enabled, all the refinement rules associated to are candidates and the firing of one leads to exclude the others.

3.3 Properties of an HTPN

In Definition 5 we formalize the soundness property of an HTPN.

.

Soundness of an HTPNAn HTPN is sound if and only if:

•
All transitions must be quasi-lives; no transition that can never be fired;
•
Each step must not be fired more than once; and
•
Final state must always be $\bot$ : for each state Tr reachable from the initial state $Tr_{0}$ , it is always possible to reach the unique final state $\bot$ . We call this property, Proper termination.

.

Each HTPN is sound.

Proof..

Pursuant to finite (the finite number of nodes component) property of the tree representing the HTPN, the absence of recursion, and soundness of nodes (because they have a TaskPN structure, which is acyclic and its source nodes are places), for demonstrating the three conditions cited in Definition 5 (about the soundness of a HTPN) it suffices to prove that: a) the firing of each transition in each node is always possible; and b) each transition in each node must not be fired more than once. By its simplified structure, it is very easy to prove that TaskPN is sound. So is the case for nodes of a HTPN, because each node has a control structure of a TaskPN. On the other hand, the choice of the refinement-rule to use did not depend on the marking; it just depends on whether the transition to refine is enabled. The firing condition of this transition depends only on the marking of active node marking where this transition is located. ∎

The soundness property implies that the number of accessible states of a HTPN is bounded. Therefore, the reachable graph is also bounded. It indicates also that all paths in the reachable graph lead to a single final state. Each path contains the refinement rules and elementary transitions (including end and fork transitions) to select in order to perform the highest level task $t_{0}$ . Among these transitions or refinement rules appearing in the reachable graph, we distinguish between two properties related to transitions:

.

Necessary and eventual transitionLet $(\mathcal{P},Tr_{0})$ be a market HTPN and t be a transition in $\mathcal{P}$ . $t$ is:

•
Necessary transition iff $t$ must be fired to reach the final state, whatever the path to take. Formally: $(Tr_{0}\xrightarrow{\sigma}Tr_{f})\wedge(\sigma=\sigma^{\prime}t\sigma^{\prime% \prime}\vee(\sigma=\sigma^{\prime}r\sigma^{\prime\prime}/r\in R_{t}))$ ;
•
Eventual transition, iff $t$ can be fired to reach the final state. Formally: $\exists\sigma/Tr_{0}\xrightarrow{\sigma}Tr_{f}\wedge(\sigma=\sigma^{\prime}t% \sigma^{\prime\prime}\vee(\sigma=\sigma^{\prime}r\sigma^{\prime\prime}/r\in R_% {t}))$ .

Necessary (respectively Eventual) transitions correspond to the tasks that must (respectively may) be performed to accomplish the task $t_{0}$ of an HTPN instance.
4. Hierarchical plans

4.1 Hierarchical-Plan-Net

HTPN is simple formalism for representing compound tasks. In this section, we extend the HTPN with information concerning the resources to consume and to produce by different tasks. The resulting model is called Hierarchical-Plan-Net (HPlNet) [2]. For this end, we make to annotate the transitions with information about the resources related to the tasks modelled by these transitions. For elementary transitions this information are specified by the designer; however, for abstract transition, it is computed and summarized (according to some computation logic) from the potential resources to consume and to produce related to the transitions of lower levels. We give below the formal definition of HPlNet (Definition 7).

.

Hierarchical-Plan-NetA Hierarchical-Plan-Net (HPlNet) is defined by the tuple: $(P,T,F,$ $W,s,e,Res,R)$ where:

•
$(P,T,F,W,s,e,R)$ is HTPN where $T=\{t_{0},e\}$ and $t_{0}$ is the single abstract transition of the highest level;
•
$Res:T\rightarrow\mathcal{R}q\times\mathcal{R}q$ is a function defining the sets of the consumption and the production associated to each transition. $\mathcal{R}q=\{(rs_{1},q_{1}),...,(rs_{n},q_{n})\}$ where $rs_{i}\in\mathcal{R}$ is resource type and $q_{i}=(x,y)$ represents the lower ( $x$ or $q_{i}^{-}$ ) and upper ( $y$ or $q_{i}^{+}$ ) quantity (or number) of $rs_{i}$ ; $\mathcal{R}$ is the set of all resources.

We denote by $Res(t).cons$ (resp. $Res(t).prod$ ) the set of the consumption and the production of the task represented by $t$ , we can also write $Res(t)=(cons,prod)$ . If $(rs_{i},q_{i})$ is associated to an elementary transition then $q_{i}^{-}=q_{i}^{+}$ . In this case, we can represent $q_{i}$ by a simple value. The end-transition and fork-transition are not related to any resource. Graphically we omit the representation of the resource sets related to fork and end-transitions. However, the set of resources to consume (resp. to produce) related to other tasks are represented just before (resp. after) their name. If we are not interested by the values of resources we represent it by ‘–’.

Figure 6 shows an instance of HPlNet representing a plan for the task Build-P (described in Section 2.1). In this example the set of resources to consume of transition Produce-q is $\{(fd,2),(M_{1},1)\}$ and the set of resource to produce is $\{(q,1),(M_{1},1)\}$ . They denote that the task Produce-q has to consume (resp. to produce) 2 units of $f d$ and 1 unit of $M_{1}$ (resp. 1 unit of $q$ and 1 unit of $M_{1}$ ). The sets of resources to consume and to produce of the transition Prepare-q are graphically represented by ‘–’. The values of these sets is derivable from elementary-transitions’ consumption and production (See Section 4.3.1).

Figure 6.
An instance of HPlNet for building the part P.

Comparing with HTPN, the concept of resource introduced in HPlNet can limit the behavior space of plans and can lead to have dead states (that cannot lead to a final state). In this context, we assume that the agents are aware of the available resources before and when the plan execution evolves. Hence, we proceed to extend the execution state to include the availability of each resource (that we call execution context). In Definition 8 we formalize the state representation.

.

State of a HPlNet

•
A state of a HPlNet $\mathcal{P}=(P,T,F,W,s,e,Res,R)$ is defined by the tuple $(Tr,Cxt)$ where: (i) $T r$ is the state of $(P,T,F,W,s,e,R)$ ; and (ii) $Cxt=\{(rs_{1},qt_{1}),...,(rs_{n},qt_{n})\}$ is a finite set of available resources, where $qt_{i}$ is the amount of resource $rs_{i}$ . We write $qt_{Cxt}(rs)$ to denote the amount of resource $r s$ in $C x t$ .
•
The initial state is $(Tr_{0},Cxt_{0})$ , such that $Tr_{0}$ is the initial state of $(P,T,F,W,s,e,R)$ and $Cxt_{0}$ is the initial state of available resources.
•
The final state is $(\bot,Cxt)$ .
•
The tuple $(\mathcal{P},(Tr_{0},Cxt_{0}))$ represents the marked HPlNet.

As the case of HTPN, a step in HPlNet concerns the execution of an elementary-transition, end-transition, or a refinement-rule. However, the execution of an elementary-transition in HPlNet must take into account the information about the resources associated to. Definition 9 summarizes the formalization of steps in HPlNet.

.

Execution conditions and execution rules in HPlNetGiven a state $(Tr,Cxt)$ , a node $n$ in $T r$ , and a step $s p$ in $n$ .

•
$s p$ is enabled in $(Tr,Cxt)$ , denoted by $(Tr,Cxt)\xrightarrow{sp}$ , iff: $Tr\xrightarrow{sp}$ and $(sp\in T_{elem}(Pl(n)))\Rightarrow\forall(rs,q)\in Res(sp).cons,qt_{Cxt}(rs)\geqslant q$ (Note that $q^{-}=q^{+}=q$ ).
•
the execution of sp leads to the state $(Tr^{\prime},Cxt^{\prime})$ , denoted by $(Tr,Cxt)\xrightarrow{sp}(Tr^{\prime},Cxt^{\prime})$ , such that:

–
$Tr\xrightarrow{sp}Tr^{\prime}$
–
$(sp\in R_{t}(Pl(n)))\Rightarrow(Cxt^{\prime}=Cxt)$
–
$(sp\in T_{elem}(Pl(n)))\Rightarrow(Cxt^{\prime}=\{(rs_{i},qt_{Cxt}(rs_{i})-q^{% \prime}_{i}+q^{\prime\prime}_{i})\})$ where $(rs_{i},q^{\prime}_{i})\in Res(sp).cons$ and $(rs_{i},q^{\prime\prime}_{i})\in Res(sp).prod$ .

We note that the only difference between the firing condition and firing rules in HTPN and HPlNet is the execution of elementary transitions. The supplementary condition for the elementary transition to be enabled concerns the availability of the amount of required resources in the current execution context. Therefore, the execution of elementary transition leads to change the marking of places in $T r$ and to change the amount of resources availability in the context according to the amount of resources to consume and to produce.

The execution of an HPlNet instance can succeed if it reaches a final state; we call the steps sequence, a run. In the execution phase, agents can check if an execution state can or cannot lead to a final state. If this state can lead to final state, we call that it is a safe state. The execution an HPlNet instance can fail if the amount of available resources is not sufficient for the execution of any transition. Hence, the current state is blocking (deadlock state). In some not-blocking state, an elementary transition can be enabled vis-a-vis $T r$ but it is not vis-a-vis $C x t$ (its required resources are unavailable in $C x t$ ). This transition is said postponed transition in this state. The fork, end, and the abstract transition will not be postponed transition because their execution is not related to resources.

We define below (Definition 10) the concepts of blocking state, safe state, postponed transition, and run.

.

Blocking state, safe state, postponed transition, and runLet $\mathcal{P}$ be a plan, represented by an HPlNet, and $(Tr_{0},Cxt_{0})$ be its initial state.

•
A state $(Tr^{\prime},Cxt^{\prime})\in[(Tr_{0},Cxt_{0})\rangle$ is blocking state iff: $\not\exists sp\in\cup_{n_{i}\in N(Tr^{\prime})}(T_{elem}(n_{i})\cup R(n_{i})),% (Tr^{\prime},Cxt^{\prime})\xrightarrow{sp}$ .
•
A state $(Tr^{\prime},Cxt^{\prime})\in[(Tr_{0},Cxt_{0})\rangle$ is safe state iff: $(Tr^{\prime},Cxt^{\prime})\xrightarrow{}(\bot,Cxt^{\prime\prime})$ and $(Tr^{\prime},Cxt^{\prime})\not\xrightarrow{}(Tr^{\prime\prime\prime},Cxt^{% \prime\prime\prime})$ such that $(Tr^{\prime\prime\prime},Cxt^{\prime\prime\prime})$ is blocking state.
•
A transition $t\in T_{elem}(n_{i})$ such that $n_{i}\in N(Tr^{\prime})$ is postponed in not blocking state $(Tr^{\prime},Cxt^{\prime})\in[(Tr_{0},Cxt_{0})\rangle$ iff $Tr^{\prime}\xrightarrow{sp}$ and $Cxt\not\xrightarrow{t}$ .
•
A run for $\mathcal{P}$ is a steps sequence $\sigma$ enabled in $(Tr_{0},Cxt_{0})$ such that $(Tr_{0},Cxt_{0})\xrightarrow{\sigma}(\bot,Cxt)$ .

A run is a safe execution (correct execution) of a HPlNet. We note that the execution of a HPlNet instance may be performed according a set of possible runs. This is justified by the presence of several refinement rules (for abstract transitions) and/or by the presence of concurrent tasks that can be executed in a different orders. The set of possible runs corresponds to all possible paths between the initial state and final state.

In the plan execution phase, some internal or external events can occur and can lead the execution context to be changed in unpredictable manner. In multi-agent systems when the execution failure can lead to critic situation, the agents should be able to continually verify if the plan execution is still in safe state. In this context of analysis, the agents should be interested in the proper termination of plans evolution from the current execution state (even if it is not reachable from the initial state). Therefore, we define the properties of sure, possible, and impossible proper termination. We define formally these properties as follows (Definition 11).

.

Sure, possible, and impossible proper terminationLet $\mathcal{P}$ a plan represented by an HPlNet and $(Tr,Cxt)$ be its current execution state. The proper termination of the execution of $\mathcal{P}$ from $(Tr,Cxt)$ is:

•
Sure, iff $(Tr,Cxt)$ is safe state and cannot lead to blocking state;
•
Impossible, iff $(Tr,Cxt)$ cannot lead to final state $(Tr,Cxt)\not\xrightarrow{}(\bot,Cxt^{\prime})$ ;
•
Possible, iff $(Tr,Cxt)$ can lead to final state, $(Tr,Cxt)\xrightarrow{}(\bot,Cxt^{\prime})$ .

4.2 Soundness of HPlNet

The soundness property as it is defined for HTPN do not take into account the concurrent task dependency because in HTPN the concurrent task are totally independent and can be executed in parallel way. In the case of HPlNet the tasks are related to shared resources, the execution on one task can postpone (when the required resources become available) or exclude the execution of another. To reflect this feature, we distinguish between two variants of soundness property: weak soundness and strong soundness. Weak soundness property is such as defined in the case of HTPN. Strong soundness is weak soundness to which add the following condition: “there will no postponed transitions”.

.

Soundness of an HPlNet A marked HPlNet $(\mathcal{P},(Tr_{0},Cxt_{0}))$ is

•
Weakly sound iff:

–
All steps must be quasi-lives. Formally: $\forall sp\in\cup_{n_{i}\in N(Tr^{\prime})}(T_{elem}(n_{i})\cup R(n_{i})),% \exists(Tr,Cxt)\in[(Tr_{0},Cxt_{0})\rangle,(Tr,Cxt)\xrightarrow{sp}$ ,
–
Each step must not be fired more than once. Formally: $\forall sp\in\cup_{n_{i}\in N(Tr^{\prime})}(T_{elem}(n_{i})\cup R(n_{i})),((Tr% ,Cxt)\in[(Tr_{0},Cxt_{0})\rangle\wedge(Tr_{0},Cxt_{0})\xrightarrow{sp}(Tr^{% \prime},Cxt^{\prime}))\Rightarrow(\nexists(Tr^{\prime\prime},Cxt^{\prime\prime% })\in[(Tr^{\prime},Cxt^{\prime})\rangle,(Tr^{\prime\prime},Cxt^{\prime\prime})% \xrightarrow{sp})$ ,
–
Proper termination: each state $(Tr,Cxt)\in[(Tr_{0},Cxt_{0})\rangle$ lead to a final state $(\bot,Cxt^{\prime})$ .

•
Strongly sound iff:

–
It is weakly sound
–
No transition may be postponed in any evolution state.

We note that the soundness of an HPlNet relaxes the criterion of the uniqueness of the final state in terms of the context $C x t$ . This is justified by the fact that the diversity of firing sequence leads to the consumption and the production of different amounts of resources.

Unlike the case of HTPN, the (weak or strong) soundness property of HPlNet is not guaranteed. The soundness of a plan represented by HPlNet depends exactly on the availability of resources in the initial state. the property related to the absence of a multiplicity of firing step is inherited from HTPN.

.

In each marked HPlNet $(\mathcal{P},(Tr_{0},Cxt_{0}))$ no step can be fired more than once.

Proof..

By contradiction, we assume that there is (at least) a step that can be fired more than once. Let sp be a step such that: $(Tr_{i},Cxt_{i})\xrightarrow{sp}(Tr_{j},Cxt_{j})$ and $(Tr_{i},Cxt_{i})\in[(Tr_{0},Cxt_{0})\rangle$ . If sp can be fired again then there can be a state $(Tr_{k},Cxt_{k})\in[(Tr_{j},Cxt_{j})\rangle$ such that $(Tr_{k},Cxt_{k})\xrightarrow{sp}$ . By definition, $(Tr_{i},Cxt_{i})\xrightarrow{sp}(Tr_{j},Cxt_{j})$ implies $Tr_{i}\xrightarrow{sp}Tr_{j}$ , and if $(Tr_{j},Cxt_{j})\xrightarrow{}(Tr_{k},Cxt_{k})$ that implies $Tr_{j}\xrightarrow{}Tr_{k}$ , then $Tr_{k}\not\xrightarrow{sp}$ , and consequently $(Tr_{k},Cxt_{k})\not\xrightarrow{sp}$ , which contradicts with $(Tr_{k},Cxt_{k})\xrightarrow{sp}$ . Therefore, sp cannot be fired more than once. ∎

.

A marked HPlNet $(\mathcal{P},(Tr_{0},Cxt_{0}))$ is bounded.

Proof..

Direct consequence of Lemma 1 and the fact that the number of steps is bounded. ∎

The boundedness of a marked HPlNet means that the number of nodes in the marking tree is limited, the places and abstract transitions in each node are bounded, and the amount of each resource in the context is limited. Boundedness of HPlNet can help to analyze the plans represented by HPlNet by exploiting their Reachability Graph.

Pursuant to Lemma 1, we may decide that a marked HPlNet is sound if it is quasi-live and its termination is proper. In fact, there is dependence between these two conditions. If there is a dead step in a marked HPlNet then the evolution of execution can lead to blocking state.

.

All transitions of a marked HPlNet $(\mathcal{P},(Tr_{0},Cxt_{0}))$ are quasi-lives (no dead) if its termination is proper.

Proof. To demonstrate Lemma 2, we proceed to assume that there is a dead transition and to demonstrate that the proper termination criterion of marked HPlNet $(\mathcal{P},(Tr_{0},Cxt_{0}))$ do not hold. We assume that there is a dead transition $t_{d}$ , then there is no a state $(Tr_{i},Cxt_{i})\in[(Tr_{0},Cxt_{0})\rangle$ where $(Tr^{\prime},Cxt^{\prime})\xrightarrow{t_{d}}$ . The evolution of $\mathcal{P}$ can reach a state $(Tr^{\prime},Cxt^{\prime})\in[(Tr_{0},Cxt_{0})\rangle$ . We distinguish two cases.

Case 1
there is a state $(Tr_{1},Cxt_{1})\in[(Tr_{0},Cxt_{0})\rangle$ where $Tr_{1}\xrightarrow{t_{d}}$ and $Cxt_{1}\not\xrightarrow{t_{d}}$ , in this case $t_{d}$ is an elementary transition and the evolution of $\mathcal{P}$ from $(Tr_{1},Cxt_{1})$ cannot lead to a final state without firing $t_{d}$ because there is no others conflicting transitions with. If there is no another enabled steps in $(Tr_{1},Cxt_{1})$ than $(Tr_{1},Cxt_{1})$ is blocking state; else the state $(Tr_{1},Cxt_{1})$ leads blocking state after the firing of these steps. Accordingly, the proper-termination criterion of $(\mathcal{P},(Tr_{0},Cxt_{0}))$ do not hold.
Case 2
there is no a state $(Tr_{1},Cxt_{1})\in[(Tr_{0},Cxt_{0})\rangle$ where $Tr_{1}\xrightarrow{t_{d}}$ . This implies that $t_{d}$ is blocked by another dead transition $t^{\prime}_{d}$ that should be fired first. If there is a state $(Tr_{2},Cxt_{2})\in[(Tr_{0},Cxt_{0})\rangle$ where $Tr_{2}\xrightarrow{t^{\prime}_{d}}$ and $Cxt_{2}\not\xrightarrow{t^{\prime}_{d}}(Tr_{2},Cxt_{2})$ is blocking state or leads to blocking state, according to the case 1. In the contrary, the case 2 is still invoked with $t^{\prime}_{d}$ . $\Box$

.

A marked HPlNet $(\mathcal{P},(Tr_{0},Cxt_{0}))$ is sound if the condition of proper termination holds.

Proof..

Pursuant to Lemma 1, in each marked $(\mathcal{P},(Tr_{0},Cxt_{0}))$ steps cannot be fired more than once. On the other hand, according to Lemma 2, the marked HPlNet is quasi-live if the condition of proper termination holds. Therefore, a marked HPlNet $(\mathcal{P},(Tr_{0},Cxt_{0}))$ is sound if the condition of proper termination holds. ∎

The most simple and intuitive method to verify that a marked HPlNet $(\mathcal{P},(Tr_{0},Cxt_{0}))$ is sound, i.e. its termination is proper, is to analyze the reachability graph. This can be done by checking that the only sink states are final states, or $(\bot,Cxt)$ . By analyzing this graph, we can also verify that $(\mathcal{P},(Tr_{0},Cxt_{0}))$ is strongly sound by checking the absence of postponed task. This is possible by verifying, for each state $st_{i}=(Tr_{i},Cxt_{i})$ , the existence of an arc for each elementary transition $t$ enabled in $Tr_{i}$ . Or:

$(Tr_{i},Cxt_{i})\xrightarrow{t}\Rightarrow\exists(Tr_{j},Cxt_{j})\in[(Tr_{i},% Cxt_{i})\rangle,(Tr_{j},Cxt_{j})\xrightarrow{t}$

The analysis of the plans by exploiting their reachability graph is inappropriate because it can cost the complexity of calculation. In addition, it does not properly exploit the multiple levels of abstraction characterizing HPlNet. The analysis can be improved by using summary information associated with abstract transitions. With this information, the verification of Soundness, Feasibility, and Invalidity properties is possible by analyzing highest level of abstraction of plans only. Pursuant to Lemma 2, we deduce that the source of dead state is the lack of required resources. Hence, de soundness property is sensitive to the initial execution context and/or and how a transition can produce resources required for the performance of others. In the next, we present some idea on how analyzing the resources requirement of a plan represented by HPlNet in order to analyze its relationship with the initial state.
4.3 Abstract reasoning on hierarchical plans

The simple and direct method consists in finding, in a first step, the set of run without taking into account the resources manipulation. In a second step, the amount of resources to consume and to produce by the set of elementary transitions is computed. Finally, the amounts of resources consumption (respectively produced) by the plan is summarized in intervals, the lower bound of each interval represents the minimum consumption (respectively production) and the upper bound represents the maximum consumption (respectively production) of all obtained runs. However, this method is not suitable and has the drawbacks of reachability graph analysis.

4.3.1 Summarizing resources consumption and production

In order to have information summarizing the conception and the production associated to a plan represented by HPlNet, we use a bottom-up method.

This one is used to compute and to use the summary information about resources to consume and to produce of elementary or abstract tasks and plan according the following semantic:

Regardless of the sequence of elementary tasks that may be carried out for performing an abstract task, the amount of each resource really consumed or produced should be comprised in the interval specified in summary information associated to this abstract task.

The following procedures (Algorithm 1) are used to compute (or deduce) the summary information of each abstract task. The procedure ComputeSN(n) (resp. ComputePN(n)) compute the summary information related to a sequential-TaskPN (resp. parallel-TaskPN) node, n, from its component tasks. These procedures call the procedure ComputeAbsT(n,t) for computing the summary information related each component task that is abstract. The procedure first(n) (resp. last(n)) returns the first (resp. the last) task in the node n. The procedure Next(n,t) (resp. prev(n,t)) returns the next (resp. previous) task having to be executed after (resp. before) the task t in the node n. Note that the potential consumption and production of resources related to an hierarchical plan represented by an HPlNet is summarized in the transition $t_{0}$ . This information can be computed in off-line manner by the procedure ComputeAbs( $n_{0},t_{0}$ ). The calculus operators $\boxplus$ , $\boxtimes$ , $\sqcup$ , and $\sqcap$ used in these procedures are described in [2].

Algorithm 1
Computation of summary information
1:
procedure ComputeSN( $n$ )
2:
$t\leftarrow last(n)$
3:
$\langle Cons,Prod\rangle\leftarrow\langle\emptyset,\emptyset\rangle$ ;
4:
repeat
5:
if $t\in T_{abs}(n)$ then
6:
ComputeAbsT( $n, t$ ) ;
7:
end if
8:
$Const\leftarrow Res(t).const\boxplus(Const\boxtimes Res(t).prod)$ ;
9:
$t\leftarrow$ prev( $n, t$ );
10:
until $t=$ null
11:
$t\leftarrow first(n)$
12:
while $t$ is not an end-transition do
13:
$Prod\leftarrow Res(t).prod\boxplus(Prod\boxtimes Res(t).cons)$ ;
14:
$t\leftarrow$ next( $n, t$ );
15:
end while
16:
Return( $C o n s, P r o d$ ) ;
17:
end procedure
1:
procedure ComputePN( $n$ )
2:
$\langle Cons,Prod\rangle\leftarrow\langle\emptyset,\emptyset\rangle$ ;
3:
for each $t\in T(n)/\{e,f\}$ do
4:
if $t\in T_{abs}(n)$ then
5:
ComputeAbsT( $n, t$ ) ;
6:
end if
7:
$Cons\leftarrow Cons\boxplus Res(t).cons$
8:
$Prod\leftarrow Prod\boxplus Res(t).prod$
9:
end for
10:
Return $\langle Cons\sqcup Prod,Prod\sqcup Cons\rangle$
11:
end procedure
1:
procedure ComputeAbsT( $n, t$ )
2:
$\langle Cons,Prod\rangle\leftarrow\langle\emptyset,\emptyset\rangle$ ;
3:
for each $(t,n_{i})\in R_{t}(n)$ do
4:
if $n_{i}$ is parallel-TaskPN then
5:
$\langle Cons_{i},Prod_{i}\rangle\leftarrow$ ComputePN( $n_{i}$ );
6:
end if
7:
if $n_{i}$ is sequential-TaskPN then
8:
$\langle Cons_{i},Prod_{i}\rangle\leftarrow$ ComputeSN( $n_{i}$ );
9:
end if
10:
$Cons\leftarrow Cons\sqcap Cons_{i}$ ;
11:
$Prod\leftarrow Prod\sqcap Prod_{i}$ ;
12:
end for
13:
$Res(t)\leftarrow\langle Cons,Prod\rangle$
14:
end procedure

Figure 7 shows calculus tree summarizing the computation of the resources to consume and to produce by the task Prepare-q (Fig. 6). In this example the set of resources to consume (resp. to produce) related to the transition Prepare-q is $\{(tl,(0,1)),(O,(0,1)),(tp,(0,1)),(fd,(0,2)),(M_{1},(0,1))\}$ (resp. $\{(tl,(0,1)),(tp,(0,1)),(q,(1,1)),(q^{\prime},(0,2)),(M_{1},(0,1))\}$ ).

Figure 7.
Calculus tree of summary information related to the transition Prepare-q (Fig. 6).

During the execution of the plans, some tasks in the plans are already executed and others not yet. In this case the potential consumption and production of resources related to an hierarchical plan must only take into account the tasks that are not yet executed. For this purpose, the summary information related to the task $t_{0}$ must be updated. For example, after the execution of the task represented by the transition Disassemble-O (Fig. 6) where $r_{3}$ is the refinement rule selected for decomposing the task Prepare-q, the information summarizing the amount of resources to consume and to produce by Prepare-q in this state is directly derived from the task Move-q-to-RM ( $Res(\verb"Prepare-q")=Res(\verb"Move-q-to-RM")$ ).

We provide in Algorithm 2 the procedures to use for updating the resources’ requirement. The procedure UpdateSN(n,Mp,Mt) (resp. UpdatePN(n,Mp,Mt)) compute the summary information related to an activated sequential-TaskPN (resp. parallel-TaskPN) node, n, from its component tasks that are not yet executed. These procedures call the procedure UpdateAbsT(n,Mt,t) for computing the summary information related each component task that is abstract. The procedure firstTran(n,Mp,Mt) returns the executing task or the first, in the node n, to be executed in the next step. The procedure Next(n,t) is the same used in Algorithm 1. The procedure prevTran(t,n,Mp,Mt)) returns the previous task having to be executed just before the task t in the node n. The potential consumption and production of resources related to an hierarchical plan represented by an HPlNet is summarized in the transition $t_{0}$ . This information can be updated, by calling the procedure UpdateAbsT(n0,Mt,t0) after the execution of each elementary task. To avoid the calculus complexity, appropriate heuristics can be used (in this paper, we omit this point).
Algorithm 2
Updating summary of information
1:
procedure UpdateSN( $n, M p, M t$ )
2:
$t\leftarrow$ FirstTran( $n, M p, M t$ );
3:
$\langle Cons,Prod\rangle\leftarrow\langle\emptyset,\emptyset\rangle$ ;
4:
while $t$ is not an end-transition do
5:
if $t\in T_{abs}(n)$ and $Mt(t)\neq\varepsilon$ then
6:
UpdateAbsT( $n, M t, t$ ) ;
7:
end if
8:
$Prod\leftarrow Res(t).prod\boxplus(Prod\boxtimes Res(t).cons)$ ;
9:
$t\leftarrow$ next( $n, t$ );
10:
end while
11:
repeat
12:
$Cons\leftarrow Res(t).cons\boxplus(Cons\boxtimes Res(t).prod)$ ;
13:
$t\leftarrow$ prevTran( $t, n, M p, M t$ ) ;
14:
until t=null
15:
Return $\langle Cons,Prod\rangle$
16:
end procedure
1:
procedure UpdatePN( $n, M p, M t$ )
2:
$TT\leftarrow\{t_{i}\in T(n)-\{f,e\}/Mp\xrightarrow{t_{i}}\vee Mp\xrightarrow{% ft_{i}}\vee Mt(t_{i})\neq\varepsilon\}$ ;
3:
$\langle Cons,Prod\rangle\leftarrow\langle\emptyset,\emptyset\rangle$ ;
4:
for each $t\in TT$ do
5:
if $t\in T_{abs}(n)$ and $Mt(t)\neq\varepsilon$ then
6:
UpdateAbsT( $n, M t, t$ );
7:
end if
8:
$\langle Cons,Prod\rangle\leftarrow\langle Cons\boxplus Res(t).cons,Prod% \boxplus Res(t).prod\rangle$ ;
9:
end for
10:
if length( $T T$ ) $>$ 1 then
11:
Return $\langle Cons\sqcup Prod,Prod\sqcup Cons\rangle$ ;
12:
else
13:
Return $\langle Cons,Prod\rangle$
14:
end if
15:
end procedure
1:
procedure UpdateAbsT( $n, M t, t$ )
2:
$\langle n^{\prime},Mp^{\prime},Mt^{\prime}\rangle\leftarrow Mt(t)$ ;
3:
if $n^{\prime}$ is parallel-TaskPN then
4:
$Res(t)\leftarrow$ UpdatePN( $n^{\prime},Mp^{\prime},Mt^{\prime}$ )
5:
end if
6:
if $n^{\prime}$ is sequential-TaskPN then
7:
$Res(t)\leftarrow$ UpdateSN( $n^{\prime},Mp^{\prime},Mt^{\prime}$ ) ;
8:
end if
9:
end procedure
4.3.2 Summary information based plans verification

One can note that the specification of resources related to tasks can implicitly characterize situations of tasks and plans interaction. Indeed, summarizing of resources information in the highest level of abstraction can lead to distinguish situations in which an agent or a multi-agent plan is conflict free, feasible, or invalid.

As all information related to the potential resources consumption of all tasks represented in HPlNet is summarized in the transition $t_{0}$ , the soundness property can be verified by directly comparing this information with the available resources in the current execution context. Admitting that the real consumption on a plan is comprised between the lower and upper bounds in the summary information, we easily prevent some properties about the soundness, feasibility, and invalidity. The conditions of these properties are formalized in the following definition.

.

Sound feasible and invalid planLet $Cxt_{0}$ be the initial execution context and $\mathcal{P}$ be a plan represented by an HPlNet. $\mathcal{P}$ is said to be :

•
Strongly sound in $Cxt_{0}$ iff $\forall(rs,q)\in Res(t_{0}).cons,qt_{Cxt_{0}}(rs)>q^{+}$ ;
•
Invalid in $Cxt_{0}$ iff $\exists(rs,q)\in Res(t_{0}).cons,qt_{Cxt_{0}}(rs)<q^{-}$ ;
•
Feasible in $Cxt_{0}$ iff $\forall(rs,q)\in Res(t_{0}).cons,qt_{Cxt_{0}}(rs)>q^{-}$ and $\exists(rs,q)\in Res(t_{0}).cons$ , $qt_{Cxt_{0}}(rs)\in[q^{-},q^{+}[$ .

During the execution phase, the execution of some tasks may be failed and therefore their resources to produce may not be carrying out. Yet the resources are produced correctly by tasks, their availability may be altered due to an unpredictable events. To cope with this issue, the plans must be verified in order to know if their executing is stills safe or not. The property to verify is proper termination. As the verification is also based on the summary information, the proper termination may be qualified as sure, possible, and impossible. Definition 14 formalize the condition of sure, possible, and impossible proper Termination.

.

Sure, possible, and impossible proper terminationLet $(Tr,Cxt)$ be the current execution state of a plan $\mathcal{P}$ represented by an HPlNet. The proper termination of the execution of $\mathcal{P}$ in $(Tr,Cxt)$ is said to be:

•
Sure, iff the state $(Tr,Cxt)$ is safe;
•
Impossible, iff the available resources in $C x t$ are not sufficient to complete all remaining subtasks. The execution of $t_{0}$ never reaches a final state. Formally: $\exists(rs,q)\in Res(t_{0}).cons,qt_{Cxt}(rs)<q^{-}$ ;
•
Possible, iff the reachability of a final state is uncertain. According to a particular order of steps firing, a final state may be reached. Formally: $\forall(rs,q)\in Res(t_{0}).cons,qt_{Cxt}(rs)>q^{-}$ and $\exists(rs,q)\in Res(t_{0}).cons,qt_{Cxt}(rs)\in[q^{-},q^{+}[$ .

5. Hierarchical plans with synchronization

5.1 HPlNet with synchronization (SHPlNet)

In this section, we present SHPlNet (Hierarchical Plan Net with Synchronization), an extension of HPlNet [3] that deals with the interaction between tasks and plans.

One can note that the execution of plans may lead to critical situations due to the potential conflict between the tasks sharing critical resources. The conflict may occur between tasks in an individual agent plan or between tasks belonging to different agents’ plans. To address these conflicting situations, the planning and coordination process has to synchronize the tasks and to promote certain decomposition methods in plans. To be able to represent plans taking into account the synchronization between tasks, we extend HPlNet by adding features allowing to impose an execution order between parallel tasks, and to avoid the activation of some refinement rules.

The idea behind SHPlNet is to add a separate module grouping synchronization and inhibition constraints. We use an ordinary Petri net, that we call synchronization net, to represent this module. The formal definition of SHPlNet is as follows (Definition 15).

.

SHPlNetHierarchical-Plan-Net with Synchronization (SHPlNet) is defined by the tuple: $(P,T,F,W,s,e,Res,R$ , $S)$ where:

•
$(P,T,F,W,s,e,Res,R)$ is HPlNet;
•
$S=(\cup_{i}P_{i}^{s},\cup_{i}T_{i}^{s},\cup_{i}W_{i}^{s},\cup_{i}F_{i}^{s})$ is a Petri net such that $(P_{i}^{s},T_{i}^{s},W_{i}^{s},F_{i}^{s})$ can have either of the following structure:

–
$(\{p,rs\},\{t_{1},t_{2}\}$ , $\{(t_{1},p),(t_{1},rs),(p,t_{2}),(rs,t_{2})\}$ , $\{((t_{1},p),1),((t_{1},rs),x)$ , $((p,t_{2}),1),((rs,$ $t_{2}),x)\})$ such that $x\leqslant q^{-}$ where $(rs,q)\in Res(t_{1}).prod$ , to represent production-consumption relationship to exchange $x$ unites of the ressource $rs\in\mathcal{R}$ between two necessary and concurrent tasks (producer and consumer) $t_{1}$ et $t_{2}$ ,
–
$(\{p\},\{t_{1},t_{2}\},\{(t_{1},p),$ $(p,t_{2})\},\{((t_{1},p),1),((p,t_{2}),1)\})$ to represent a temporal order between two necessary and concurrent tasks $t_{1}$ and $t_{2}$ ,
–
$(\{p\},\{r\},$ $\{(p,r)\},\{((p,r),1)\})$ to represent an inhibition of a refinement rule $r\in R_{t}$ for an abstract and necessary task $t$ defined in HPlNet. $R_{t}\cap T(S)\neq R_{t}$ .
–
Each transition defined in $T(S)$ is a transition or a refinement rule defined in HPlNet.

The Petri net S defined in Definition 15 constitutes a coordination module including synchronization constraints that enforce an execution order and ensure the exchange of some quantities of resources between concurrent tasks (explicit positive interaction). It includes also constraints that enforce the selection of one refinement rule.

One can note that several causal relationships can be related to the same resource that is represented by a unique place. In order to protect the amounts of resources to be exchanged between different peers of transitions (producers and consumers), we propose to add, for each causal relationship, a second temporal constraint between the same transitions (using another place). This additional constraint allows the producer task to notify the availability of expected amount of resource to the consumer task.

Note also, that synchronization constraints concern only the necessary tasks (or transitions). This is motivated by the fact that these constraints are handled at run time in the planning or coordination phases where the agents should take some decisions regarding the selection of a particular refinement rule or serialization of concurrent tasks. For adding a synchronization constraint between tasks, agent (s) must firstly commit to ensure that these tasks must be executed to carry out the global task $t_{0}$ . The same condition must be hold in the case of refinement rule. In the instance of SHPlNet illustrated in Fig. 2, there is an inhibition constraints of the refinement rule $\verb"r"_{6}$ , a synchronization constraint between the transitions Produce-L and Produce-H, and a production-consumption relationship between the transitions Produce-H and Produce-q.
5.1.1 Semantic of SHPlNet

The particularity of HPlNet semantic is related to the manipulation of the resources by tasks. The particularity of SHPlNet semantic is related to the manner the tasks in agent or multi-agent plans can be positively or negatively interfered. As the case of HPlNet, the execution semantic of SHPlNet is described in terms of the states and transition between states. However, the state representation of a SHPlNet takes into account the state of the synchronization net, which allows to exchange control information between concurrent tasks and to impose an additional constraint on refinement rules selection.

Therefore, the state a SHPlNet is represented by the extended marking (Definition 16) that deals with state of hierarchical tasks, state of available resources, and state of synchronization net.

.

State of a SHPlNetA state of SHPlNet $\mathcal{P}=(P,T,F,W,s,e,Res,R,S)$ is defined by the tuple $(Tr,Cxt,Ms)$ such that

•
$(Tr,Cxt)$ is the state of HPlNet $(P,T,F,W,s,e,Res,R)$ .
•
$M s$ is a marking of $S$ , the initial and final marking of $S$ is $Ms_{0}=0$ .
•
The initial state is $(Tr_{0},Cxt_{0},0)$ such that $(Tr_{0},Cxt_{0})$ is the initial state of $(P,T,F,W,s,e,Res,$ $R)$ .
•
The final state is $(\bot,Cxt_{f},0)$ .

The steps of SHPlNet are firing of an elementary-transition, end-transition, or refinement-rule. Definition 17 below states respectively the execution condition and execution rules.

.

Execution condition and execution rules in SHPlNetGiven a state $(Tr,Cxt,Ms)$ , a node $n$ in $T r$ , and a step $s p$ in $n$

•
$s p$ is enabled in $(Tr,Cxt,Ms)$ , denoted by $(Tr,Cxt,Ms)\xrightarrow{sp}$ , iff:

$(i)$
$(Tr,Cxt)\xrightarrow{sp}$ ,
$(ii)$
$sp\in T_{s}\Rightarrow Ms\xrightarrow{sp}$ ,
$(iii)$
$sp\in R_{t}(n)\wedge t\in T_{s}\Rightarrow Ms\xrightarrow{t}$ .

•
The execution of a step $s p$ leads to the state $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})$ , denoted by $(Tr,Cxt,Ms)\xrightarrow{sp}(Tr^{\prime},Cxt^{\prime},Ms^{\prime})$ , such that:

$(iv)$
$(Tr,Cxt)\xrightarrow{sp}(Tr^{\prime},Cxt^{\prime})$ ,
$(v)$
$sp\in T_{elem}(Pl(n))\Rightarrow(sp\in T_{s}\Rightarrow Ms\xrightarrow{sp}Ms^{% \prime})\wedge(sp\not\in T_{s}\Rightarrow Ms^{\prime}=Ms)$ ,
$(vi)$
$sp\in R_{t}(Pl(n))\Rightarrow(t\in T_{s}\Rightarrow(\forall p\in P_{s},Ms^{% \prime}(p)=Ms(p)-W_{s}((p,t))))\wedge(t\not\in T_{s}\Rightarrow Ms^{\prime}=Ms)$ ,
$(vii)$
$sp=e(Pl(n))\wedge nischildofn^{\prime}byr=(t^{\prime},Pl(n))\Rightarrow(t^{% \prime}\in T_{s}\Rightarrow(\forall p\in P_{s},Ms^{\prime}(p)=Ms(p)+W_{s}(t^{% \prime},p))\wedge(t^{\prime}\not\in T_{s}\Rightarrow Ms^{\prime}=Ms)$ .

In Definition 17, the condition (ii) states that all possible steps appearing in $S$ cannot be enabled if they are not enabled in $M s$ . The condition (iii) states that an abstract transition appearing in $S$ cannot be decomposed if it is not enabled in $M s$ . The condition (v) states that the execution of an elementary transition appearing in $S$ implies its firing in S. The condition (vi) states that the execution of refinement rule of a transition that appear in $S$ implies to the consumption of tokens. The production of the tokens will be after the firing of end transition of the node refining the abstract transition (condition (vii)).

The properties of blocking state, safe state, postponed transition, run, sure, possible, and impossible proper Termination are refined in Definitions 18 and 19.

.

Blocking state, safe state, postponed transition, and runLet $\mathcal{P}$ be a plan, represented by a SHPlNet, and $(Tr_{0},Cxt_{0},Ms_{0})$ be its initial state.

•
A state $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})\in[(Tr_{0},Cxt_{0},Ms_{0})\rangle$ is blocking state iff: $\nexists sp\in\cup_{n_{i}\in N(Tr^{\prime})}(T_{elem}(n_{i})\cup R(n_{i})),(Tr% ^{\prime},Cxt^{\prime},Ms^{\prime})\xrightarrow{sp}$
•
A state $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})\in[(Tr_{0},Cxt_{0},Ms_{0})\rangle$ is safe state iff: $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})\xrightarrow{}(\bot,Cxt^{\prime\prime},0)$ and $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})\not\xrightarrow{}(Tr^{\prime\prime% \prime},Cxt^{\prime\prime\prime},Ms^{\prime\prime\prime})$ such that $(Tr^{\prime\prime\prime},Cxt^{\prime\prime\prime},Ms^{\prime\prime\prime})$ is blocking state
•
A transition $t\in T_{elem}(n_{i})$ such that $n_{i}\in N(Tr^{\prime})$ is postponed in not blocking state $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})\in[(Tr_{0},Cxt_{0},Ms_{0})\rangle$ iff $Tr^{\prime}\xrightarrow{sp}\wedge Ms^{\prime}\xrightarrow{sp}\wedge Cxt^{% \prime}\not\xrightarrow{t}$
•
A run for $\mathcal{P}$ is a steps sequence $\sigma$ enabled in $(Tr_{0},Cxt_{0},0)$ such that $(Tr_{0},Cxt_{0},0)\xrightarrow{\sigma}(\bot,Cxt,0)$

.

Sure, possible, and impossible proper terminationLet $\mathcal{P}$ a plan represented by an SHPlNet and $(Tr,Cxt,Ms)$ be its current execution state. The proper termination of the execution of $\mathcal{P}$ from $(Tr,Cxt,Ms)$ is:

•
Sure, iff $(Tr,Cxt,Ms)$ is safe state and cannot lead to blocking state;
•
Impossible, iff $(Tr,Cxt,Ms)$ cannot lead to final state $(Tr,Cxt,Ms)\not\xrightarrow{t}(\bot,Cxt^{\prime},0)$ .
•
Possible, iff $(Tr,Cxt,Ms)$ can lead to final state, $(Tr,Cxt,Ms)\xrightarrow{t}(\bot,Cxt^{\prime},0)$ .

5.1.2 Summary information in a SHPlNet

If there are no constraints between concurrent tasks, the used technique for computing summary information in an HPlNet may be applied in case of a SHPlNet. For example, the task Produce-H&L in Fig. 8(i) can be refined by three partially ordered tasks, Produce-H and Produce-L. The summary information related to Produce-H&L can be derived from these tasks as is outlined in Section 4.3. However, if there are synchronization constraints between Produce-H and Produce-L, as the case of Fig. 8(ii) the technique must be modified. With this constraint, Produce-H and Produce-L are viewed as totally ordered tasks.

Figure 8.

Influence of synchronization net on the computation of the summary information.

In fact, the synchronization net in SHPlNet is considered as a set of rewriting rules that rewrite the control flow structure of the nodes. The application semantic of these rules is equivalent to the imbrications of parallel and sequential-TaskPN. The propagation of summary information to higher levels tasks should take into account the fact that the quantity to be produced (resp. consumed) is not cumulative because it is intended to (resp. provided by) another non-local tasks (do not belong to the same node). Thus, for a producer (resp. consumer) task $t$ of $x$ unites of a resource $r s$ in profit of (resp. provided by) a non-local task $t^{\prime}$ , the quantity of $r s$ to propagate $Q_{prod}$ (resp. $Q_{cons}$ ) is computed as follows:

$\displaystyle Q_{prod}=(q^{-}-x,q^{+}-x)\ \text{such that}\ (rs,q^{-},q^{+})% \in\ \text{Res(t).prod}$ $\displaystyle Q_{cons}=(q^{-}+x,q^{+}+x)\ \text{such that}\ (rs,q^{-},q^{+})% \in\ \text{Res(t).cons}$

Finally, the inhibitions constraints allow simply to ignore the blocked refinement rules when calculating summary information for an abstract task. The calculation procedure addresses this refinement rule as if it no longer exists.

5.2 Soundness of SHPlNet

The consideration of concurrent tasks synchronization leads to the redefinition of the conditions under which a hierarchical plan is sound. Establishing temporal order relationships and exchange of resources between parallel tasks can lead to reduced consumption of resources, which can lead therefore to obtain a sound plan. However, it may also be a source of the occurrence of cycles, which lead always to blocking states.

In the same way as a plan represented by HPlNet, a plan represented by SHPlNet can be analyzed from an abstract level. Based on the summary information associated to transitions, agents can decide that the proper termination of their plan execution is sure, possible, or impossible, provided that this plan is cycles free. As synchronization constraints are applied only on necessary tasks, the cycles lead always to deadlock state that prevents the execution of any task in plans. Before defining the cycle concept, we define the execution order relationship between two steps $sp_{1}$ and $sp_{2}$ , noted $sp_{1}\prec sp_{2}$ , which means that $sp_{2}$ must be executed after the execution of $sp_{1}$ is finished.

.

Execution order( $\prec$ )Let $\mathcal{P}$ be a SHPlNet, $sp_{1}$ and $sp_{2}$ be two steps, and $n_{1}$ and $n_{2}$ two nodes in $\mathcal{P}$ . $sp_{1}\prec sp_{2}$ , iff either of the following condition holds:

•
$\{(sp_{1},p),(p,sp_{2})\}\in F(S(\mathcal{P}))$ ,
•
$\{(sp_{1},p),(p,sp_{2})\}\in F(n_{1})$ ,
•
$sp_{1}\prec t\wedge sp_{2}\in R_{t}(n_{1})$ ,
•
$sp_{1}\in R_{t}(n_{1})\wedge sp_{1}=(t,n_{2})\wedge\{s(n_{2})\}=\bullet sp_{2}$ ,
•
$sp_{1}=e(n_{2})\wedge\{(t,n_{2})\}=R_{t}(n_{1})\wedge t\prec sp_{2}$ .

We define formally a cycle and acyclic plan property as follows.

.

Cycle in SHPlNet and acyclic planLet $\mathcal{P}$ be a SHPlNet and $\{sp_{0},sp_{1},$ … $,sp_{m}\}$ be a set of steps.

•
The list $\langle sp_{0},sp_{1},...,sp_{m},sp_{0}\rangle$ forms a cycle in $\mathcal{P}$ iff: $\forall i\in\{0,1,\ldots,m\},t_{i}\prec t_{(i+1)mod(m)}$
•
$\mathcal{P}$ is said to be acyclic or cycles free iff do not include cycles. Else it is said to be cyclic

For example if the synchronisation net in Fig. 2 is replaced by that in Fig. 9 results an instance of cyclic SHPlNet. In this case, the cycle is: $\langle\verb"Produce-L",$ $\verb"Produce-H",e4,\verb"Produce-q",e5,\verb"Build-P-From"\linebreak\verb"-q"% ,e3,\verb"Build-Q",\verb"Build-P",r2,\verb"Produce-L"\rangle$ .

Figure 9.
Instance of a synchronisation net.

We note that soundness of a SHPlNet is relaxed as far as the absence of dead steps. Precisely, the blocked refinement rules and the transitions belonging to the nodes related to are excluded from the condition of “no dead steps”. This relaxation is benefit in the agent and multi-agent planning context. If in some situations some execution alternatives are not suitable, the agent (s) can commit to block these alternatives. In this case, all tasks related to are considered non-existent. Therefore, we mean by "all transitions should be quasi-live" the transitions that are not excluded.

The verification of soundness property of an acyclic SHPlNet is only limited to the verification of quasi-liveness property of all steps (that are not excluded) and proper termination property, because the property relative to the absence of multiple firing of steps is inherited directly from HPlNet model.

.

A marked SHPlNet $(\mathcal{P},(Tr_{0},Cxt_{0},0))$ does not contain steps that can be fired more than once.

Proof..

By contradiction, we assume that there is (at least) a step that can be fired more than once. Let sp be a step such that $(Tr_{i},Cxt_{i},Ms_{i})\xrightarrow{sp}(Tr_{j},Cxt_{j},Ms_{j})$ and $(Tr_{i},Cxt_{i},Ms_{i})\in[c)\rangle$ . If $s p$ can be fired again, then there is $(Tr_{k},Cxt_{k},Ms_{k})\in[(\mathcal{P},(Tr_{j},Cxt_{j},Ms_{j}))\rangle$ such that $(Tr_{k},Cxt_{k},Ms_{k})\xrightarrow{sp}$ . By definition $(Tr_{i},Cxt_{i},Ms_{i})\xrightarrow{sp}(Tr_{j},Cxt_{j},Ms_{j})$ implies $Tr_{i}\xrightarrow{sp}Tr_{j}$ , and if $(Tr_{j},Cxt_{j},Ms_{j})\xrightarrow{}(Tr_{k},Cxt_{k},Ms_{k})$ that implies $Tr_{j}\xrightarrow{}Tr_{k}$ then $Tr_{k}\not\xrightarrow{sp}$ , and consequently $(Tr_{k},Cxt_{k},Ms_{k})\not\xrightarrow{sp}$ , which contradicts with $(Tr_{k},Cxt_{k},Ms_{k})\xrightarrow{sp}$ . Therefore, $s p$ cannot be fired more than once. ∎

.

A marked SHPlNet $(\mathcal{P},(Tr_{0},Cxt_{0},0))$ is bounded.

Proof..

Direct consequence of Lemma 3 and the fact that the number of steps is bounded. ∎

Pursuant to Lemma 3, we can decide that an acyclic SHPlNet is (weakly or strongly) sound if it is quasi-live and proper termination property is verified. As the case of a marked HPlNet, in fact, there is a dependency between these two properties. If there is a dead step in a marked SHPlNet than the evolution of marking can lead to not proper termination state (or blocking state).

.

All transitions of a marked acyclic SHPlNet $(\mathcal{P},(Tr_{0},Cxt_{0},0))$ are quasi-lives (no dead) if its termination is proper.

Proof. To demonstrate Lemma 4, we proceed to assume that there is a dead transition and to demonstrate that the proper termination condition of marked SHPlNet $(\mathcal{P},(Tr_{0},Cxt_{0},0))$ do not hold. We assume that there is a dead transition $t_{d}$ , then there is no state $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})\in[(Tr_{0},Cxt_{0},0)\rangle$ where $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})\xrightarrow{t_{d}}$ . The evolution of $\mathcal{P}$ can reach a state $(Tr^{\prime},Cxt^{\prime},Ms^{\prime})\in[(Tr_{0},Cxt_{0},0)\rangle$ . We distinguish two cases.

Case 1:
there is a state $(Tr_{1},Cxt_{1},Ms_{1})\in[(Tr_{0},Cxt_{0},0)\rangle$ where $(Tr_{1},Ms_{1})\xrightarrow{t_{d}}$ and $Cxt_{1}\not\xrightarrow{t_{d}}$ , in this case $t_{d}$ is an elementary transition and the evolution of $\mathcal{P}$ from $(Tr_{1},Cxt_{1},Ms_{1})$ cannot lead to a final state without firing $t_{d}$ because there is no others conflicting transitions with. If there is no another enabled steps in $(Tr_{1},Cxt_{1},Ms_{1})$ than $(Tr_{1},Cxt_{1},Ms_{1})$ is blocking state; else the state $(Tr_{1},Cxt_{1},Ms_{1})$ leads blocking state after the firing of these steps. Accordingly, the proper-termination criterion of $(\mathcal{P},(Tr_{0},Cxt_{0},0))$ do not hold.
Case 2:
there is no a state $(Tr_{1},Cxt_{1},Ms_{1})\in[(Tr_{0},Cxt_{0},0)\rangle$ where $Tr_{1}\xrightarrow{t_{d}}$ . This implies that $t_{d}$ is blocked by another dead transition $t^{\prime}_{d}$ that should be fired first. If there is a state $(Tr_{2},Cxt_{2},Ms_{2})\in[(Tr_{0},Cxt_{0},0)\rangle$ where $(Tr_{2},Ms_{2})\xrightarrow{t^{\prime}_{d}}$ and $Cxt_{2}\not\xrightarrow{t^{\prime}_{d}}$ , $(Tr_{2},Cxt_{2},Ms_{2})$ is blocking state or leads to blocking state, according to the case 1. In the contrary, the case 2 is still invoked with $t^{\prime}_{d}$ . $\Box$

.

A marked SHPlNet $(\mathcal{P},(Tr_{0},Cxt_{0},0))$ is sound if the condition of proper termination holds.

Proof..

Pursuant to Lemma 3, in each marked $(\mathcal{P},(Tr_{0},Cxt_{0},0))$ steps cannot be fired more than once. On the other hand, according to Lemma 4, the marked SHPlNet is quasi-live if the condition of proper termination holds. Therefore, a marked SHPlNet $(\mathcal{P},(Tr_{0},Cxt_{0},0))$ is sound if the condition of proper termination holds. ∎

In the previous section, we showed how to verify the soundness of a plan represented by HPlNet by only analyzing the summary information associated with the task of highest abstraction level. The condition used for this is not sufficient for the case of SHPlNet due to the possible occurrence of the cycles causing deadlock situations. Therefore, the absence of cycles in a plan represented by SHPlNet is a necessary condition to be sound.

In Definition 22, we formulate conditions in which the proper termination of plan execution is sure, possible, or impossible

.

Sure, possible and impossible for proper terminationLet $(Tr,Cxt,Ms)$ be an execution state of a plan $\mathcal{P}$ . The proper termination of the execution (or simply the execution termination) of $\mathcal{P}$ is:

•
Sure, iff $\mathcal{P}$ is acyclic and $\forall(rs,q)\in Res(t_{0}).cons,qt_{Cxt}(rs)\geqq+$ ,
•
Impossible, iff is $\mathcal{P}$ is cyclic or $\exists(rs,q)\in Res(t_{0}).cons,qt_{Cxt}(rs)<q^{-}$ ,
•
Possible, iff $\mathcal{P}$ is acyclic and $\forall(rs,q)\in Res(t_{0}).cons,qt_{Cxt}(rs)>q^{-}$ and $\exists(rs,q)\in Res(t_{0}).cons,qt_{Cxt}(rs)\in[q^{-},q^{+}[$ .

A plan whose execution is impossible is a plan that has no way to ensure the success of its execution. A plan whose the safe execution is sure is a flexible plan. It can be executed correctly regardless of the choice to be taken to refine abstract transitions and the execution order of concurrent tasks. Between these two cases, the success of execution may be possible in an uncertainty case. To address this incertitude, the plan must be reorganized by updating the synchronization net (block some refinement rules and/or add some constraints on the execution of tasks).
6. Related works

In this paper, we are not interested in the multi-agent systems verification. My work here concerns a new idea for verifying and validating an agent and multi-agent plans that are executed in complex and dynamic environment. We are exactly interested in dynamic verification of flexible plans when a team of interacting agents has to automatically and continually plan, execute, and monitor their actions.

In the most classical multi agents planning, the verification is inherently accomplished during the elaborating of plans, planning, and coordination. The used planning and coordination algorithms try to, a priori, find (making a means-end analysis) plan that will be valid. These approaches can be considered as generative verification. However, the proposed works to deal with verification as a problem are not much. In the following, we present those that are closely related to the work presented in this paper.

In [14] Gordon proposed an framework for dynamic plans adaptation where the (re)verification is required in order to ensure that critical behavioral constraints are always satisfied after every adaptation. The verification of plan, which is represented as finite-state automaton, is required after adaptation operation not when executing plan become infeasible. The proposed (re) verification algorithm, which is based on model-checking approach, is incremental and it is called after the application of each updating operator. The idea of incremental (re) verification and the idea introduced to localize the (re) verification to gain speed are beneficial. Although the model of the plan used in this work does not manipulate metric resources, its verification localization idea can complement our work. We can propose to analyze in a preliminary step the tasks defined in an abstract level and separate them into subsets of tasks, which can be verified independently. If the work of Gordon aims to improve the efficiency of reverication after learning, so that agents have a sufficiently rapid response time, our verification approach is proposed to be used to improve the efficiency of (re) planning, (re) coordination, and execution monitoring. In contrast to Gordon, we have used hierarchical plans and exploited the abstraction in the verification process to challenge the dynamic verification problem during planning and execution phase.

Recursive Petri net proposed by Seghrouchni and Haddad in [18] is a more expressive formalism to represent hierarchical plans. The distinction between abstract and primitive transitions and the firing rules principles are all features enabling to verify the feasibility of hierarchical plan. While its power to express a wide range of agent plans, the recursive Petri net suffers from the inability to explicitly represent the interaction and interdependence of concurrent tasks and its inability to reason on abstract tasks. The verification of plan, that is required during the coordination phase, can be used during the execution. The proposed verification or validation process is based on the analysis of the reachability tree that must enumerate all possible execution instances. Unlike Seghrouchni and Haddad, we proposed to better exploit the abstraction in the verification of hierarchical plans that manipulate metric resources. We proposed combining the verification based on the analysis of the summary information with one based on the analysis of the reachability graph. We note that the verification based on the analysis of reachability graph suffer from high complexity, especially when the plans are partially refined. To deal with this problem, many work proposed to enrich the plans representation models or to use control structure for enhance the verification process.

Fallah-Seghrouchni and Degirmenciyan-Cartault have proposed in [12] a framework for controlling the execution of the multi-agent plan and its validation. They propose mechanism for extract the pertinent constraints for the execution of the plans in order to control their execution and finally to dynamically validate it. These pertinent constraints are considered as information summarizing the conditions related to resources required for plan execution. Similar to our framework, this information is used to verify some properties about the validity and the quality of plan and to control its execution ability in the current execution context. Fallah-Seghrouchni and Degirmenciyan-Cartault have adopted the formalism of Hybrid Automata (formalism based on the extension of timed automata) to model the different variables of agents’ plans. This formalism allows model-checking of important properties like reachability, security, liveness, deadlock absence, $\ldots$ However, the plans have one level of abstraction and must be complete to be checked. The verification process requires decomposition of individual plans of the agents and enumerating all runs associated to. In contrast to Fallah-Seghrouchni and Degirmenciyan-Cartault framework, we proposed to compute summary information for a partial hierarchical plans rather for partial order plans (as in [12]). The validation technique that we proposed does not require explicitly enumerating all runs associated to hierarchical plans.

In [17] Muise et al. have proposed an execution monitoring (EM) technique that enables to monitor, as a plan is being executed, the action execution and the world state in order to identify the discrepancy between the predicted and observed execution outcome. A central task of EM system is to verify whether a partial plan being executed remains valid (feasible in the case of our framework) with respect to certain state. This work was especially dealing with the problem of partial-order plans (POP) execution monitoring. Partial-order plans are considered as a compact representation for multiple linearizations of actions. The authors exploit the notion of regression, defined in [13] for total ordered plan, to identify the conditions that ensure the validity of a POP. The overal idea is similar to the work proposed in [12], but without enumerating all linearization of actions. The regression concept is used to summarize, for each action, the condition in which it is executable. The dynamic verification is only accomplished by comparing the condition associated to action with execution state. The idea of associating with each action the summary information on the rest of the actions that are not yet executed is beneficial, it may reduce the complexity of the verification and may gain speed the reaction of agents. However, incorporate into plans a large amount of information can make its size large and its elaboration becomes therefore complex. In our approach, we are insisting on the minimization of summary information so that the adaptation of the plans is fast. In our work, for computing the required resources for parallel or sequential tasks, we used two concepts regression, and progression. The regression concept is used for computing the set of resources to consume and the progression concepts is used for computing the set of resources to produce. As we used in our framework hierarchical plans, we proceed to compute the summary conditions horizontally and vertically according to hierarchical plan structure. We used a computing technique that enables interacting agents to cope with the interference of their plans without having to analyze all plans actions.

To enable interacting agents to verify the hierarchical plans (that are considered as a compact representation for multiple linearization of actions) by analysis as much theirs abstract levels, we proceed to propagate the information about the conditions and the resources, related to elementary tasks, towards the abstract tasks. This idea is closely related to the those introduced by Clement et al. [6]. Clement et al. proposed the model CHiPs (for concurrent hierarchical plans) by annotating each task in hierarchical plans with summary information specifying the conditions in which these tasks can be accomplished. By comparing this information with an execution context, the agents can verify the viability of their plans. Based on the same idea, Thangarajah et al. have introduced [19] Goal-Plan-Tree. While it is proposed as an agent-based model, it is closely similar to Clement and Durfee approach, concerning the use of summary information to handle interaction between concurrent goals. However, the proposed models in all these works are not appropriate to address the evolution aspect of plans, especially in a dynamic environment. Our inspiration by Petri net allows us to remedy this deficiency and to have a formal framework for analyzing the plans evolution. The verification technique proposed in this paper can combine the analysis based on summary information and those based on reachability graph analysis.

7. Conclusion

The work presented in this paper concerns the verification of agent and multi-agents hierarchical plans. We have interested in how to enable interacting agents to be able to continually verify the soundness of their plans, monitor the evolution of their execution and environment, and better switch between local planning, coordination, and execution. For this end, we presented new computational techniques to verify soundness, feasibility, and invalidity properties of executing partial plans (represented by SHPlNet) by analyzing their abstract level of representation. We proofed that to verify that a plan (multi-agent) is sound or invalid, it is enough to compare the whole requirement of the plan (summary at the abstract level) with all available resources. However, the use of the same technique for the feasibility property is not decisive. A feasible plan may be invalid because the technique to use to summary its consumption and production is not safeguarding some crucial information. To avoid any ambiguity about feasible property, the reachability technique can be (partially) used. In fact, the use our technique to reason about hierarchical plans is proposed to be used in conjunction with reachability graph based analysis technique, that is a central in the field of Petri net. This approach of verification enables interacting agents to make progressive verification. In a first step, the extremes properties, soundness and invalidity are verified, if these properties are not holding, the agents analyze the reachability graph in a second step.

Verification based on the analysis of information summarizing the consumption and production of tasks in terms of resources gives an idea of the impact of context (resources available) on the successful completion of the plans execution. Moreover, verification based on the analysis of abstract level of plan is much preferred in the multi-agent systems in the sense that it enable to make it possible to preserve the private nature of the individual agents’ plans. An agent unveils the details on his plans with only those with plans in strong correlation (determined based on the summary information) to his.

Yet I am part of the observations indicating the contribution of abstraction (as mentioned in the related works section), there are some questions that were not addressed in this paper and that we will focus on in the near future work. Firstly, the analysis of the computational complexity is not argued here. We will show how the summary information based analysis can reduce the computational complexity compared to the reachability graph. We will especially concentrate on the impact of summary information updating on the rapidly responsive of agents to handle unpredictable events. Moreover, the modular verification will be investigated in the future works. The summary information available in the abstract levels can be used to identify tasks interaction and therefore the set of tasks the agent can local verify without taking into account the others. We can also investigate the use summary information in definition of abstract reachability graph, those including abstract states produced when the execution of an abstracts tasks is abstracted. This idea could be widely exploited in the multi-agent coordination and monitoring.

Footnotes

HTPN: Hierarchical Task Petri Net; HPlNet: Hierarchical Plan Net.

Authors’ Bios

Brahimi Said was born on May 27, 1977 in Algeria. Brahimi Said received the Engineer’s degree in Computer Science from University of Constantine, Algeria, in 2000. He received the Master degree in Computer Science from the same university in 2003. He received his PhD in Computer Sciences at University of Constantine 2 (Algeria) in 2014. At present, he is a professor at the Department of Computer Science, University of Guelma, 8 mai 1945 (Algeria). His research interests are mainly in the areas of multi-agent system and distributed artificial intelligence.

Ramdane Maamri is an associate professor of computer science in University of Constantine 2, Algeria. He received his master from University of Minnesota, USA, and his Ph.D in Computer Science from University of Mentouri Constantine, Algeria. He has participated in a lot of national and international research projects and supervised a lot of masters and Ph.D students. He is currently the head of Software Technologies and Information Systems Department and his research interests include software engineering, verification and validation, web services, multi agent systems and ambient systems.

Sahnoun Zaidi is a full professor of Computer Science in University of Constantine 2, Algeria. He received his master and Ph.D in Computer Science from Rensselaer Polytechnic Institute in U.S.A. He has held various positions in both the academic and administrative field and has conducted a lot of national and international research projects. He supervised a lot of masters and Ph.D students. He is currently the dean of the New Technologies of Information and Communication Faculty and his research interests includes software engineering, fuzzy logics, formal methods, multi agent systems and complex systems.

References

Alami

Robert

Ingrand

F.F.

and Suzuki

, Multi-robot cooperation through incremental plan-merging, in: IEEE Int. Conf. on Robotics and Automation, Japan, 1995, pp. 2573–2578.

Brahimi

Maamri

and Sahnoun

, Hierarchical Multi-Agent Plans Using Model-Based Petri Net, International Journal of Agent Technologies and Systems, IGI Global 5(2) (2013), 1–30.

Brahimi

Maamri

and Sahnoun

, Partially centralized approach for dynamic hierarchical-plans merging, Neurocomputing 146 (2014), 187–198.

Christensen

and Petrucci

, Modular analysis of Petri nets, The Computer Journal 43(3) (2000), 224–242.

Clement

B.J.

and Barrett

A.C.

, Continual coordination through shared activities, in: Proceedings of the second international joint conference on Autonomous agents and multiagent systems, ACM, Australia, 2003, pp. 57–64.

Clement

B.J.

Durfee

E.H.

and Barrett

A.C.

, Abstract reasoning for planning and coordination, Journal of Artificial Intelligence Research 28 (2007), 453–515.

de Jonge and Roos

, Plan-execution health repair in a multi-agent system, in: Proceedings of the 23rd Workshop of the UK Planning and Scheduling Special Interest Group, 2004, pp. 33–44.

desJardins

and Wolverton

, Controlling communication in distributed planning using irrelevance reasoning, in: Proceedings of the Fifteenth National Conference on Artificial Intelligence, 1998, pp. 868–874.

Durfee

E.H.

Ortiz, Jr

C.L.

and Wolverton

M.J.

, A survey of research in distributed, continual planning, Ai Magazine 20(4) (1999), 13.

10.

Erol

, Hierarchical Task Network Planning: Formalization, Analysis, and Implementation, Ph.D. thesis, College Park, MD, USA, 1996.

11.

Erol

Hendler

and Nau

D.S.

, Semantics for hierarchical task-network planning. Technical report CS-TR-3239, UMIACS-TR-94-31, Computer Science Dept., University of Maryland, March 1994.

12.

Fallah-Seghrouchni

A.E.

Degirmenciyan-Cartault

and Marc

, Modellingcontrol, and validation of multi-agent plans in dynamic context, in: Autonomous Agents and Multiagent Systems, Proceedings of the Third International Joint Conference on. IEEE, 2004, pp. 44–51.

13.

Fritz

and McIlraith

S.A.

, Monitoring Plan Optimality During Execution, in: Proceedings of the 17th International Conference on Automated Planning and Scheduling, 2007, pp. 144–151.

14.

Gordon

D.F.

, Asimovian adaptive agents, Journal of Artificial Intelligence Research 13 (2000), 95–153.

15.

Haddad

and Poitrenaud

, Recursive petri nets, Acta Informatica 44(7–8) (2007), 463–508.

16.

Seghrouchni

A.E.F.

and Haddad

, A coordination algorithm for multi-agent planning, in: European Workshop on Modelling Autonomous Agents in a Multi-Agent World, Springer Berlin Heidelberg, 1996, pp. 86–99.

17.

Muise

McIlraith

S.A.

and Beck

J.C.

, Monitoring the execution of partial-order plans via regression, in: Proceedings of the International Joint Conference On Artificial Intelligence, 2011, pp. 1975–1982.

18.

Seghrouchni

A.E.F.

and Haddad

, A recursive model for distributed planning, in: Proceedings of the 2nd International Conference on Multi-Agent Systems, 1996, pp. 307–314.

19.

Thangarajah

Padgham

and Winikoff

, Detecting and Avoiding Interference Between Goals in Intelligent Agents, in: International Joint Conference on Artificial Intelligence, 2003, pp. 721–726.