- In multi-agent systems evolving in complex and dynamic environments, the agents need to plan their tasks and to monitor its execution in order to deal with unpredictable situations. They must have plans that remain subject to continual updating, even during its execution. To cope with this issue, we proposed in previous works, SHPlNet, a model allowing to represent plans less sensitive to execution contexts, and to support run-time validation and verification. This paper aims to present a theoretical framework for the verification and validation of soundness and invalidity properties of partial hierarchical plans by analyzing their abstract level representation.
In multi-agent systems, planning can allow
agents to reason about their actions and
interactions. In this context, plans can be used as
procedures for resolving specific problems.
Agents can be provided by plans as reusable
procedural knowledges enabling them to behave
in similar situations or conditions. Techniques
used in this context are based on case based
reasoning approach [
In order to deal with the dynamics of complex environments, planning and execution must be interleaved. This is motivated by the following requirements:
To reduce the time between the deliberation and the execution of actions to prevent these actions from becoming obsolete at the time of their execution; To reduce the complexity of planning and coordination by reducing the search space; To have information about the execution context through the execution of certain fragments plans.
To be able to succeed interleaving planning and
execution, the agents must be able to reason
about partially refined plans. They must be able
also to take the appropriate decision regarding
the initiation, suspension, repair, and the
execution resuming of certain fragments of plans
while continuing the execution of other's.
In previous works [
This paper aims to provide theoretical framework
for analyzing and verifying agent and multi-agent
plans at run-time. We explain and demonstrate
how to verify the soundness property of partial
plan by analyzing only its abstract level.
In fact, there are some key related works that
dealt with this question, like as [
The work proposed in [
The rest of this paper is structured as follows. Section 2 outline the key properties related to partial plans. In section 3, we present preliminary formalism, HPlNet, (Hierarchical-Plan--Net) and the underlying properties. In section 4, we illustrate the representation of hierarchical plans and its synchronization. We also explain and demonstrate how to verify these plans. Finally, we conclude our paper.
REQUIREMENT
In multi-agent systems where the planning and execution process are interleaved, agents must be able to represent, verify (and validate), and monitor partial plans at run-time. They must be able to verify the following properties: Soundness: soundness property denotes that the plan: - Must not contain dead tasks. It is generally not important to incorporate unnecessary tasks in a plan; - Should not contain tasks that can be performed more than once. Therefore, only one instance of a plan requires at most one instance for each task or decomposition method; and - Must be completely executed. It must be correctly refined to ground and executable plans. Its execution must not lead to blocking situations.
For multi-agent plan, the soundness property denotes that there is no conflict between the tasks of one or more individual plans Flexibility: a flexible plan is a sound one that can be refined to several (at least two) ground plans. Therefore, its execution can be flexible. Feasibility: a plan is feasible if it can be executed correctly. A partial plan is called feasible if it can be refined to at least one executable and complete plan.
Invalidity: a plan is invalid if it cannot be executed correctly. A partial plan is called invalid if it cannot be refined to any executable and complete plan. For multi-agent plan, the Invalidity property denotes that the plan contains an unsolvable conflict between tasks (of one or more individual plans).
Agents that interleave planning and execution must be able to identify and to verify these properties in order to behave in an appropriate manner and to take suitable decision about the initiation, suspension, repair, and execution resuming of certain (fragments of) plans while continuing the execution of others. 3. SIMPLE HIERARCHICAL PLANS
REPRESENTATION
In this section, we present the formalism used to
represent simple hierarchical plans where the
tasks are hierarchically organized. For more
detail about the hierarchical plan representation,
the reader can refer to [
3.1.1.
In this subsection, we provide a formalism, that we call Hierarchical Plan net (HTPN), to represent hierarchical plans based on extension of Petri net. The key idea consists of defining a tree-based structure. Each node in this tree is a special Petri net representing totally and partially ordered tasks networks. Formal definition of HTPN is as follow.
A Hierarchical-Task-Petri-Net (HTPN) is defined by the tuple where is a Petri net, and:
is a finite set of transitions, disjoint union of elementary and abstract transitions . may be empty;
is a particular place representing the source place ( );
is a particular transition representing the end transition ( );
, is a finite set of refinement rules for all abstract transitions ( ); each rule associates to a transition a refinement HTPN. denotes the set of all rules can be used to refine the task ;
is a Petri net to have either of the following two structures: - All transitions and places belong to a single path from to , i.e.
, , and
. in this case, is called Sequential-Task
- All transitions (except and ) belong to parallel flows initiated by a fork transition f (having a single entry place ), and should be joined by the end-transition , i.e. , , , the tasks are connected to source place by a fork transition . in this case, is called Parallel-Task
A HTPN may be considered as a tree of nodes. The root of this tree is where and , is highest-level task of . The leaves of the tree are nodes where ( ). The intermediate nodes are characterized by ( ). Abstract transitions model abstract (or compound) tasks and elementary transitions model atomic (or elementary) tasks.
As we explained above, the HTPN may be viewed as a tree of nodes having TaskPN structure. Hence, the state of HTPN must take into consideration the marked places of these nodes. The state of HTPN must also take into account the refinement state of abstract tasks. We hence extend the marking concept of ordinary Petri net to define a marking that deals with the characteristic of HTPN (definition 2). Definition 2 (Extended marking of HTPN). An extended marking of HTPN is defined by the tree such that is the set of node; each node is a tuple such that is a node in ; , and ( denotes the absence of tokens) is a marking function of abstract transitions; is the root of tree; a node is the child of in if and only if such that , and One can note that: - The tree structure of is implicitly defined, a node is the child of in iff such that , and . - The initial extended marking is such that where , , and is the initial marking (where ); - The final marking, , is an empty tree (that has no node), noted by .
The extended marking of HTPN is considered as a state indicating the activated nodes and the state of each place and each abstract transition in these nodes. A step between two marking states and , denoted by a step concerns the firing of elementary transition, endtransition, or (selected) refinement-rule. The firing will be possible only if the transition or the refinement rule is enabled (Definition 3). Definition 3 (Firing conditions in HTPN).
In the definition 4, we formalize firing rules. Definition 4 (Firing rules of HTPN).
Let be an extended marking and be a node in , the firing of a step leads to the , – , : :
and and is child of by : The concept of extended marking, enabled transition (or refinement rule), and firing rules in HTPN allow to have explicit representation of hierarchical task state and its evolution.
We present some properties of HTPN, especially the soundness property.
Definition 5 (soundness of an HTPN). An HTPN is sound iff: - There are no dead transitions: all transitions must be quasi-lives; - Each step must not be fired more than once; - Proper termination: for each state reachable from the initial state , it is always possible to reach the unique final state .
Proof. Pursuant to finite (the finite number of nodes component) character of the tree representing the HTPN, the absence of recursion, and soundness of nodes (because they have a structure TaskPN), for demonstrating the three conditions cited in the 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 extended markings 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 task , the highest level of abstraction. Among these transitions or refinement rules appearing in the reachable graph, we want to distinguish between two types of transitions: Definition 6 (Necessary and Eventual transition).
- Necessary Transition iff must be fired to reach some final state, whatever path to take. ; - Eventual transition, iff can be fired to reach a final state. Formally: be a
and Necessary transitions correspond to the tasks that must be performed to accomplish the task of a plan. However, Eventual transitions correspond to the tasks that may be performed to accomplish the task of a plan.
We provide a formalism, that we call Hierarchical-Plan-Net (HPlNet), making an As the case of HTPN, a step in HPlNet concerns an elementary-transition, end-transition, or a refinement-rule. However, the steps firing in HPlNet must take into account the summary information about the resources associated to the transitions. The formalization of steps firing in HPlNet is summarized by definition 9 and 10. Definition 9 (Firing conditions in HPlNet). Given an extended marking , a node in , a step is enabled in , denoted by
, Case 2: and ). Definition 10 (Firing rules in HPlNet). Let be an extended marking, be a node in , the firing of a step leads to the extended marking , denoted by , such that: extension of HTPN by adding information about the resources to consume and to produce. The formal definition is given below (definition 7). Definition 7 (Hierarchical-Plan-Net).
A Hierarchical-Plan-Net (HPlNet) is defined by the tuple where:
is HTPN where and is the single abstract transition of the highest level;
is a function defining the sets of the consumption and the production associated to each transition. where is resource name and represents the lower ( or ) and the upper ( or ) quantity (number) of . is the set of all resources.
We denote by (resp. ) the set of the consumption and the production of the task represented by , we can also write . If is associated to an elementary transition then . In this case, we can represent by a simple value. The end-transition and fork-transition are not related to any resource. Hence, if is one of these two kinds of transitions then
. Graphically we omit the representation of the empty sets related to the fork and endtransitions.
The state of HPlNet is represented by an extended marking that inherits all features of state representation of HTPN, and takes into account the state of the available resources (that we call execution context). Its formal definition is as follows (definition 8).
Definition 8 (Extended marking of HPlNet). An extended marking of HPlNet is defined by the tuple where: is the
The initial extended marking is defined by , such that is the initial extended marking of and is the initial state of available resources. The final extended marking is in which is an empty tree (that has no node). The tuple represents the marked HPlNet. such that and We note that the only difference between the firing rules in HTPN and HPlNet is the firing of elementary transitions whose execution context must be updated according to the amount of resources to consume and produce. 3.2.2.
If the soundness property of HTPN is ensured, the 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 (initial context ). Therefore, the soundness checking of an HPlNet is only limited to the verification of quasi liveness property of all transitions and proper termination criterion, because the property on the absence of a multiplicity of firing step is inherited from HTPN. We note that the soundness of an HPlNet relaxes the criterion of the uniqueness of the sinks state in terms of the context, . This is justified by the fact that the diversity of firing sequence leads to the consumption and production of different amounts of resources.
there is no step 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 a step such that: there
. If can .
and can be fired again then be a state
such that
By implies definition, then Therefore, that implies , and consequently cannot be fired more than once.∎ , . is
The boundedness of 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 the lemma 1, we may decide that HPlNet is sound if it is quasi-live and proper termination criterion is checked.
In fact, there is dependence between these two criteria. Each termination of HPlNet, that is not proper, is termination when there are steps (exactly transitions) which cannot be fired, i.e. blocking.
Proof. To demonstrate that the proper termination criterion of marked HPlNet holds if it is quasi-live, we proceed to assume that the proper termination criterion did not hold and demonstrate that HPlNet is not quasi-live. We assume that the termination is not proper, then, there exists a sink state reachable from the initial state such that . By projecting HPlNet on HTPN and according to the theorem 1, if then there must be at least one firing sequence (containing steps that have not been fired) such that . Therefore, if the state is sink then the sequence must begin with an elementary transition that is enabled vis-a-vis Tr, but not enabled ( ), so and then is a dead transition, so HPlNet is not quasi-live. ∎ Theorem 3. A marked HPlNet sound if all its transitions are quasi-lives. is Proof. Pursuant to the lemma 1, in each marked steps cannot be fired more than once. On the other hand, according to the lemma 2, the proper termination holds if the marked HPlNet is quasi-live. So marked HPlNet is sound if it is quasi-live. ∎ The most simple and intuitive method to verify that a marked HPlNet is sound, i.e. is quasi-live, is to analyze the reachability graph. This can be done by checking that each transition or refinement rule belongs to a path from the initial state , and leads to a terminal and sink state .
In this regard, we define (Definition 11) the concepts of run, feasibility, flexibility, safe state, and invalidity.
Definition 11 (run, feasibility, flexibility and safe state, invalidity).
Let be a plan represented by an HPlNet and be an initial execution context: - A run for (decisions) is an enabled steps sequence in , such that ; - is executable in the context , or its execution is feasible, iff there is at least a run for it ; - is flexible in the context iff it is sound and have several runs (at least two) ; - A state reachable from
is safe-state iff there is steps sequence such that
is invalide in the the context no run. ; if it has A run is a safe execution of an HPlNet. We note that HPlNet is associated with a set of possible runs. This is justified by the presence of several refinement rules (for an abstract transition) and/or by the presence of concurrent tasks that can be triggered in a different order. The set of possible runs correspond to all possible paths between the initial extended marking and final extended markings.
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. Plans analysis can be improved by using summary information associated with the abstract transitions. With this information, the verification of certain key properties is possible by analyzing highest level of abstraction of plans only.
By projecting on the analysis of executing plan, we propose some properties on the proper termination of its evolution. This concerns the safe, possible, and impossible termination. These properties are defined as follows. Definition 12 (safe, possible, and impossible proper Termination).
Let be the current execution state of a plan represented by an HPlNet. The proper termination of the execution of in is: - safe, iff the state is safe; - Impossible, iff the available resources in are not sufficient to complete all remaining subtasks. The execution of never reaches an final state: ; - Possible, iff the reachability of a final state is uncertain. According to a particular order of steps firing, a final state may be reached : and . 4. HIERARCHICAL PLANS WITH
SYNCHRONIZATION
4.1. HPlNet with synchronization (SHPlNet)
In this section, we present SHPlNet (Hierarchical
Plan Net with Synchronization), an extension of
HPlNet [
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 tasks in the plans must be synchronized and some decomposition methods must be avoided. 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 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.
with Synchronization (SHPlNet), its formal definition is as follows (definition 13).
either of the following structure: by
Synchronization the tuple:
is a can have such that where
, to represent a productionconsumption relationship to exchange unites of the resource between two necessary and concurrent tasks (a producer and a consumer); to represent a temporal order between two necessary and concurrent tasks, and ; - to represent an inhibition of a refinement rule for an abstract and necessary task t. - Each transition defined in is a transition or a refinement rule defined in HPlNet.
The Petri net defined in the definition 13 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 consumer task. The state of plan represented by SHPlNet is modeled by the extended marking of SHPlNet (definition 14) that takes into account marking state of synchronization net.
Definition 14 (extended marking of SHPlNet). such that: An extended marking of SHPlNet is defined by the tuple is the extended marking of HPlNet
; and is a marking of ; the initial and the final marking of is .
The steps of SHPlNet are firing of an elementary-transition, end-transition, or refinement-rule. The definition 15 and 16 below state respectively the firing condition and firing rules.
Definition 15 (firing condition in SHPlNet). Given an extended marking node in , a step , a is enabled in (i) (ii) (iii) , denoted by ; ; . In the definition 15, the condition (ii) states that all possible steps appearing in cannot be enabled if they are not enabled in . The condition (iii) states that an abstract transition appearing in cannot be refined if it is not enabled in .
Definition 16 (firing rules in SHPlNet). Let be an extended marking, be a node in , the firing of a step leads to the extended marking , denoted by , if and only iff:
: , and
: ; and : ; and ; ; ; ; ; .
and is child of by
Case 2:
Case 3: In the definition 16 the case 1 states that the firing on an elementary transition appearing in leads to its firing in . The case 2 states that the firing of refinement rule of a transition that appear in leads 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 (case 3).
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 about the resources associated to transitions, we can decide that the proper termination of plan execution is sure, possible, or impossible, provided that this plan is cycles free. The cycles lead always to deadlock state that prevents the execution of any task of . We formally define the concept of cycle and acyclic plan as follows.
Definition 17 (Cycle in SHPlNet and Acyclic
Plan).
Let be SHPlNet and , be two nodes in . includes a cycle represented by
, iff: (i) for each and such that
, (ii) for each such that such that , or , or and
, or and .
such that , and
is called acyclic iff it is cycles free.
In the definition 18 we formulate the conditions in which the proper termination of plan execution will be sure, possible, or impossible Definition 18 (Sure, Possible and Impossible for Proper termination).
Let be an execution state of a plan . The proper termination of the execution (or simply the execution termination) of is: - Sure, iff is acyclic and +, - Impossible, iff is is cyclic or , - Possible, iff is acyclic and and a A plan whose execution is impossible is a plan that has no way to ensure the success of plan 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).
The consideration of concurrent tasks synchronization leads to the redefinition of the conditions under which a hierarchical plan is sound. Establishing the 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 leads to deadlock in cyclic plans.
The verification of soundness property of a SHPlNet is only limited to the verification of quasi-liveness property of all transitions and proper termination criterion, because the property relative to the absence of multiple firing of steps is inherited directly from HPlNet model. Lemma 4. A marked SHPlNet 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 be step such that then
and . If
there . By definition implies can be fired again
is such that and therefore cannot be fired Lemma 5. The proper termination criterion of marked SHPlNet is verified if it is quasi-live.
Proof. To demonstrate that the proper termination criterion of a SHPlNet is verified if it is quasi-live, we assume that the proper termination criterion of a SHPlNet is not verified and demonstrate that it is not quasi-live. We assume that the termination is not proper. Then, there exists a sink state reachable from the initial state such that . By projecting SHPlNet on HTPN and pursuant to the theorem 1, if then it must be at least one firable sequence (including steps that are not yet fired) such that . Thus, if is sink state then the first step in must be a transition which is enabled vis-avis , but it is not vis-a-vis (or ); thus and then is blocking transition. In conclusion, SHPlNet is not quasi-Live. ∎
4.
A marked SHPlNet is sound if it is quasi-live.
Proof. Pursuant to the lemma 4, there is no marked SHPlNet that can contain steps to be fired more than once. On the other hand, pursuant to the Lemma 5, proper termination criterion is verified if a marked SHPlNet is quasi-live. Therefore, the marked SHPlNet is sound if it is quasi-live. ∎ In the previous section, we showed how to verify the soundness of a plan represented by HPlNet by analyzing only 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 for it to be sound. 5. CONCLUSION The work presented in this paper complement our previous works about the representation of hierarchical plans with synchronization. We presented here a theoretical framework for the verification and validation of soundness and invalidity properties of partial hierarchical plans represented by SHPlNet. We are focused on the demonstration of some key properties that allow to verify the soundness and invalidity of plans by only analyzing the summary information than . Thus, Pursuant to the lemma 4, we can decide that SHPlNet is sound if it is quasi-live and proper termination criterion is verified. In fact, there is a dependency between these two criteria. Each termination of SHPlNet, that is not proper, is termination when there are steps (exactly transitions) which cannot be fired, i.e. blocking. associated to the task of highest abstraction level.
Future work will focus on the analysis of the computational complexity. We will show how the summary information based analysis can reduce the computational complexity compared to the reachability graph analysis. 6. REFERENCES