=Paper=
{{Paper
|id=Vol-1294/paper8
|storemode=property
|title=Validation and Verification of Agent and Multi-agent Plans in Dynamic Environment
|pdfUrl=https://ceur-ws.org/Vol-1294/paper8.pdf
|volume=Vol-1294
|dblpUrl=https://dblp.org/rec/conf/icaase/BrahimiMS14
}}
==Validation and Verification of Agent and Multi-agent Plans in Dynamic Environment==
https://ceur-ws.org/Vol-1294/paper8.pdf
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
Validation and Verification of agent and
multi-agent plans in dynamic environment
Said Brahimi Ramdane MAAMRI, Zaidi SAHNOUN
University of Guelma, Algeria University of Constantine 2
BP 24401, Guelma, Algeria Ali Mendjeli - BP : 67A, Constantine –Algeria
brahimi.said@yahoo.fr {rmaamri, sahnounz}@yahoo.fr
Abstract – 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.
Keywords – multi-agent plan verification and validation, plans analysis, dynamic planning, planning and execution
interleaving.
- To reduce the time between the deliberation
1. INTRODUCTION and the execution of actions to prevent these
actions from becoming obsolete at the time of
In multi-agent systems, planning can allow their execution;
agents to reason about their actions and - To reduce the complexity of planning and
interactions. In this context, plans can be used as coordination by reducing the search space;
procedures for resolving specific problems.
Agents can be provided by plans as reusable - To have information about the execution
procedural knowledges enabling them to behave context through the execution of certain
in similar situations or conditions. Techniques fragments plans.
used in this context are based on case based
To be able to succeed interleaving planning and
reasoning approach [1]. Furthermore, the plans
execution, the agents must be able to reason
serve as a guide that can help the agent to
about partially refined plans. They must be able
monitor its evolution in order to meet its goals
also to take the appropriate decision regarding
(means-end reasoning). They also serve as a
the initiation, suspension, repair, and the
means for predicting future situations. Finally,
execution resuming of certain fragments of plans
plans serve as a tool for coordinating and
while continuing the execution of other's.
monitoring activities for a set of agents [7]. By
anticipating the actions of other agents, an agent In previous works [10,11], we provided a
can adjust and adapt its plan to avoid harmful formalism called SHPlNet that allows to
behaviors and to benefit from the synergy of its represent hierarchical plans with multiple
plan with those of others. abstraction levels, by extending the Petri net and
by taking advantage of HTN planning [4], CHiP
In order to deal with the dynamics of complex
[3], and the modular analysis of Petri nets idea
environments, planning and execution must be
[9]. SHPlNet can take into account the
interleaved. This is motivated by the following
representation of flexible plans, and offers the
requirements:
necessary features allowing to monitor plans
evolution, to handle plans interaction and
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 73
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
interdependency, and to control resources the underlying properties. In section 4, we
evolution at run time. Furthermore, SHPlNet can illustrate the representation of hierarchical plans
allow a modular representation of plans. Firstly, and its synchronization. We also explain and
there is a clear distinction between the demonstrate how to verify these plans. Finally,
abstraction levels of hierarchical plan. Secondly, we conclude our paper.
there is clear separation between tasks and
synchronization constraints. Within this aspect,
the analysis of plans can be done in a modular 2. AGENT AND MULTI-AGENT PLAN
way, and therefore, their updating may be REQUIREMENT
simplified. Note that the modular representation In multi-agent systems where the planning and
of the plan can facilitate the revision of some
execution process are interleaved, agents must
decisions of planning and coordination in order to
be able to represent, verify (and validate), and
best meet the evolutionary aspect of the system.
These aspects are suitable to support the monitor partial plans at run-time. They must be
interleaving of planning, execution, and able to verify the following properties:
coordination. Soundness: soundness property denotes that
This paper aims to provide theoretical framework the plan:
for analyzing and verifying agent and multi-agent - Must not contain dead tasks. It is generally
plans at run-time. We explain and demonstrate not important to incorporate unnecessary
how to verify the soundness property of partial tasks in a plan;
plan by analyzing only its abstract level. - Should not contain tasks that can be
In fact, there are some key related works that performed more than once. Therefore, only
dealt with this question, like as [8, 6, 2, 5,12,13]. one instance of a plan requires at most one
Recursive Petri net proposed in [8] and extended instance for each task or decomposition
in [6] is a more expressive formalism to represent method; and
hierarchical plans. The distinction between - Must be completely executed. It must be
abstract and primitive transitions and the firing correctly refined to ground and executable
rules principles are all features enabling to verify plans. Its execution must not lead to blocking
many properties of only complete plans. While its situations.
power to express a wide range of agent plans, For multi-agent plan, the soundness property
the recursive Petri net suffers from the inability to denotes that there is no conflict between the
explicitly represent the interaction and tasks of one or more individual plans
interdependence of concurrent tasks and its
inability to reason on abstract tasks. Flexibility: a flexible plan is a sound one that
can be refined to several (at least two) ground
The work proposed in [5] is based on the idea of
plans. Therefore, its execution can be flexible.
propagating the information about related
resources for each plan. This information is used Feasibility: a plan is feasible if it can be
to verify some properties about the validity and executed correctly. A partial plan is called
the quality of plan and to control its execution in feasible if it can be refined to at least one
some context. They used formalism based on executable and complete plan.
the extension of timed automata. Similar to the
formalism used here [10], the hybrid automata Invalidity: a plan is invalid if it cannot be
allows model-checking of important properties executed correctly. A partial plan is called invalid
like reachability, security, liveness, deadlock if it cannot be refined to any executable and
absence… however, the plans have one level of complete plan. For multi-agent plan, the
abstraction and must be complete to be checked. Invalidity property denotes that the plan contains
In [12, 2, 13] the authors provided a framework an unsolvable conflict between tasks (of one or
for representing the plan based on the Petri net. more individual plans).
In these works, the plans are represented at one Agents that interleave planning and execution
level of abstraction. Like the previous works, must be able to identify and to verify these
these approaches are not suitable to represent properties in order to behave in an appropriate
and to check partial plans. manner and to take suitable decision about the
The rest of this paper is structured as follows. initiation, suspension, repair, and execution
Section 2 outline the key properties related to resuming of certain (fragments of) plans while
partial plans. In section 3, we present preliminary continuing the execution of others.
formalism, HPlNet, (Hierarchical-Plan--Net) and
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 74
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
3. SIMPLE HIERARCHICAL PLANS , the tasks are
REPRESENTATION connected to source place by a fork
In this section, we present the formalism used to transition . in this case,
represent simple hierarchical plans where the is called Parallel-Task-
tasks are hierarchically organized. For more Petri-Net (Parallel-TaskPN) node.
detail about the hierarchical plan representation, A HTPN may be
the reader can refer to [11]. considered as a tree of nodes. The root of this
tree is where and
3.1. Hierarchical Tasks , is highest-level task of . The
leaves of the tree are nodes where
3.1.1. Hierarchical-Task-Petri-Net (HTPN)
( ). The intermediate nodes are
In this subsection, we provide a formalism, that characterized by ( ). Abstract
we call Hierarchical Plan net (HTPN), to transitions model abstract (or compound) tasks
represent hierarchical plans based on extension and elementary transitions model atomic (or
of Petri net. The key idea consists of defining a elementary) tasks.
tree-based structure. Each node in this tree is a
As we explained above, the HTPN may be
special Petri net representing totally and partially
viewed as a tree of nodes having TaskPN
ordered tasks networks. Formal definition of
structure. Hence, the state of HTPN must take
HTPN is as follow.
into consideration the marked places of these
Definition 1 (HTPN). nodes. The state of HTPN must also take into
A Hierarchical-Task-Petri-Net (HTPN) is defined account the refinement state of abstract tasks.
by the tuple where We hence extend the marking concept of
is a Petri net, and: ordinary Petri net to define a marking that deals
with the characteristic of HTPN (definition 2).
- is a finite set of transitions,
Definition 2 (Extended marking of HTPN).
disjoint union of elementary and
An extended marking of HTPN is defined by
abstract transitions . may be
the tree such that is the set of
empty;
node; each node is a tuple
- is a particular place representing the such that is a node in ; ,
source place ( ); and ( denotes the
- is a particular transition representing absence of tokens) is a marking function of
the end transition ( ); abstract transitions; is the root of tree; a
- , is a finite set node is the child of in if and only if
of refinement rules for all abstract transitions such that
( ); each rule
, and
associates to a transition a
refinement HTPN. denotes the set of all One can note that:
rules can be used to refine the task ;
- The tree structure of is implicitly defined, a
- is a Petri net to have either of the
following two structures: node is the child of in iff
- All transitions and places belong to a such that ,
single path from to , i.e. and .
, , and - The initial extended marking is such that
where ,
. in this case, , and is the initial marking
is called Sequential-Task- (where );
Petri-Net (Sequential-TaskPN) node - The final marking, , is an empty tree (that
- All transitions (except and ) belong to has no node), noted by .
parallel flows initiated by a fork transition f
The extended marking of HTPN is considered as
(having a single entry place ), and should
a state indicating the activated nodes and the
be joined by the end-transition , i.e.
state of each place and each abstract transition
, ,
in these nodes. A step between two marking
states and , denoted by ,
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 75
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
concerns the firing of elementary transition, end- Proof. Pursuant to finite (the finite number of
transition, or (selected) refinement-rule. The nodes component) character of the tree
firing will be possible only if the transition or the representing the HTPN, the absence of
refinement rule is enabled (Definition 3). recursion, and soundness of nodes (because
they have a structure TaskPN), for
Definition 3 (Firing conditions in HTPN). demonstrating the three conditions cited in the
Given an extended marking , a node in , definition 5 (about the soundness of a HTPN) it
a step is enabled in , denoted by , iff: 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
In the definition 4, we formalize firing rules. very easy to prove that TaskPN is sound. So is
the case for nodes of a HTPN, because each
Definition 4 (Firing rules of HTPN). node has a control structure of a TaskPN. On
Let be an extended marking and be a node the other hand, the choice of the refinement-rule
in , the firing of a step leads to the to use did not depend on the marking; it just
extended marking , denoted by , depends on whether the transition to refine is
such that: enabled. The firing condition of this transition
Case 1: : depends only on the marking of active node
marking where this transition is located. ∎
-
– and The soundness property implies that the number
- of accessible states of a HTPN is bounded.
Therefore, the reachable extended markings
Case 2: : 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
Case 3: and is child of by distinguish between two types of transitions:
:
- , Definition 6 (Necessary and Eventual
- transition).
- Let be a market HTPN and be a
Particular case: : transition in . is:
The concept of extended marking, enabled - Necessary Transition iff must be fired to
transition (or refinement rule), and firing rules in reach some final state, whatever path to take.
HTPN allow to have explicit representation of
Formally:
hierarchical task state and its evolution.
;
3.1.2. Properties of HTPN - Eventual transition, iff can be fired to reach
a final state. Formally: and
We present some properties of HTPN, .
especially the soundness property.
Necessary transitions correspond to the tasks
Definition 5 (soundness of an HTPN). that must be performed to accomplish the task
An HTPN is sound iff: of a plan. However, Eventual transitions
- There are no dead transitions: all transitions correspond to the tasks that may be performed
must be quasi-lives; to accomplish the task of a plan.
- Each step must not be fired more than once;
- Proper termination: for each state reachable 3.2. Hierarchical Plan
from the initial state , it is always possible to
3.2.1. Hierarchical-Plan-Net (HPlNet)
reach the unique final state .
Theorem 1. Each HTPN is sound. We provide a formalism, that we call
Hierarchical-Plan-Net (HPlNet), making an
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 76
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
extension of HTPN by adding information about As the case of HTPN, a step in HPlNet concerns
the resources to consume and to produce. The an elementary-transition, end-transition, or a
formal definition is given below (definition 7). refinement-rule. However, the steps firing in
HPlNet must take into account the summary
Definition 7 (Hierarchical-Plan-Net). information about the resources associated to
A Hierarchical-Plan-Net (HPlNet) is defined by the transitions. The formalization of steps firing
the tuple where: in HPlNet is summarized by definition 9 and 10.
- is HTPN where Definition 9 (Firing conditions in HPlNet).
and is the single abstract transition of the Given an extended marking , a node
highest level; in , a step is enabled in , denoted
- is a function defining the
by , iff:
sets of the consumption and the production
associated to each transition. - and
where is -
resource name and represents the (Note that
lower ( or ) and the upper ( or ) ).
quantity (number) of . is the set of all Definition 10 (Firing rules in HPlNet).
resources. Let be an extended marking, be a
node in , the firing of a step leads to the
We denote by (resp. )
extended marking , denoted by
the set of the consumption and the production of
the task represented by , we can also write , such that:
. If is associated to Case 1:
an elementary transition then . In this
- ;
case, we can represent by a simple value. - such that
The end-transition and fork-transition are not , and
related to any resource. Hence, if is one of .
these two kinds of transitions then
. Graphically we omit the representation of Case 2: or
the empty sets related to the fork and end- - ;
transitions. - .
The state of HPlNet is represented by an We note that the only difference between the
extended marking that inherits all features of firing rules in HTPN and HPlNet is the firing of
state representation of HTPN, and takes into elementary transitions whose execution context
account the state of the available resources (that must be updated according to the amount of
we call execution context). Its formal definition is resources to consume and produce.
as follows (definition 8).
3.2.2. Properties of HTPN
Definition 8 (Extended marking of HPlNet).
An extended marking of HPlNet If the soundness property of HTPN is ensured,
is defined by the tuple the soundness property of HPlNet is not
where: guaranteed. The soundness of a plan
- is the extended marking of represented by HPlNet depends exactly on the
; availability of resources in the initial state (initial
- is a finite set of context ). Therefore, the soundness
available resources, where is the amount checking of an HPlNet is only limited to the
of resource . We write to denote verification of quasi liveness property of all
the amount of resource in . transitions and proper termination criterion,
because the property on the absence of a
The initial extended marking is defined by multiplicity of firing step is inherited from HTPN.
, such that is the initial extended We note that the soundness of an HPlNet
marking of and is the relaxes the criterion of the uniqueness of the
initial state of available resources. The final sinks state in terms of the context, . This is
extended marking is in which is an justified by the fact that the diversity of firing
empty tree (that has no node). The tuple sequence leads to the consumption and
represents the marked HPlNet. production of different amounts of resources.
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 77
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
Lemma 1. In marked HPlNet must begin with an elementary transition that is
there is no step that can be fired more than enabled vis-a-vis Tr, but not enabled
once. ( ), so and then is a dead
transition, so HPlNet is not quasi-live. ∎
Proof. By contradiction, we assume that there is
(at least) a step that can be fired more than Theorem 3. A marked HPlNet is
once. Let a step such that: sound if all its transitions are quasi-lives.
and Proof. Pursuant to the lemma 1, in each marked
. If can be fired again then steps cannot be fired more than
there can be a state once. On the other hand, according to the
such that lemma 2, the proper termination holds if the
marked HPlNet is quasi-live. So marked HPlNet
. By definition,
is sound if it is quasi-live. ∎
implies , and if
The most simple and intuitive method to verify
that implies , that a marked HPlNet is sound,
then , and consequently . i.e. is quasi-live, is to analyze the reachability
Therefore, cannot be fired more than once.∎ graph. This can be done by checking that each
Theorem 2. A marked HPlNet is transition or refinement rule belongs to a path
from the initial state , and leads to a
bounded.
terminal and sink state .
Proof. Direct consequence of the Lemma 1.∎
In this regard, we define (Definition 11) the
The boundedness of HPlNet means that the concepts of run, feasibility, flexibility, safe state,
number of nodes in the marking tree is limited, and invalidity.
the places and abstract transitions in each node
are bounded, and the amount of each resource Definition 11 (run, feasibility, flexibility and
in the context is limited. Boundedness of HPlNet safe state, invalidity).
can help to analyze the plans represented by Let be a plan represented by an HPlNet and
HPlNet by exploiting their Reachability Graph. be an initial execution context:
Pursuant to the lemma 1, we may decide that - A run for is an enabled steps sequence
HPlNet is sound if it is quasi-live and proper (decisions) in , such that
termination criterion is checked. ;
In fact, there is dependence between these two - is executable in the context , or its
criteria. Each termination of HPlNet, that is not execution is feasible, iff there is at least a
proper, is termination when there are steps run for it ;
(exactly transitions) which cannot be fired, i.e. - is flexible in the context iff it is sound
blocking. and have several runs (at least two) ;
- A state reachable from
Lemma 2. The proper termination criterion of is safe-state iff there is steps sequence
marked HPlNet holds if all its such that ;
transitions are quasi-lives. - is invalide in the the context if it has
Proof. To demonstrate that the proper no run.
termination criterion of marked HPlNet A run is a safe execution of an HPlNet. We note
holds if it is quasi-live, we that HPlNet is associated with a set of possible
proceed to assume that the proper termination runs. This is justified by the presence of several
criterion did not hold and demonstrate that refinement rules (for an abstract transition)
HPlNet is not quasi-live. We assume that the and/or by the presence of concurrent tasks that
termination is not proper, then, there exists a can be triggered in a different order. The set of
sink state reachable from the initial possible runs correspond to all possible paths
state such that . By projecting HPlNet between the initial extended marking and final
on HTPN and according to the theorem 1, if extended markings.
then there must be at least one firing The analysis of the plans by exploiting their
sequence (containing steps that have not reachability graph is inappropriate because it
been fired) such that . Therefore, if the can cost the complexity of calculation. In
state is sink then the sequence addition, it does not properly exploit the multiple
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 78
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
levels of abstraction characterizing HPlNet. use an ordinary Petri net, that we call
Plans analysis can be improved by using synchronization net, to represent this module.
summary information associated with the We call the new formalism Hierarchical-Plan-Net
abstract transitions. With this information, the with Synchronization (SHPlNet), its formal
verification of certain key properties is possible definition is as follows (definition 13).
by analyzing highest level of abstraction of plans
only. Definition 13 (SHPlNet).
Hierarchical-Plan-Net with Synchronization
By projecting on the analysis of executing plan, (SHPlNet) is defined by the tuple:
we propose some properties on the proper where
termination of its evolution. This concerns the is HPlNet; is a
safe, possible, and impossible termination.
Petri net such that can have
These properties are defined as follows.
either of the following structure:
Definition 12 (safe, possible, and impossible -
proper Termination).
Let be the current execution state of a such that where
plan represented by an HPlNet. The proper , to represent a production-
termination of the execution of in is: consumption relationship to exchange
unites of the resource between two
- safe, iff the state is safe; necessary and concurrent tasks (a producer
- Impossible, iff the available resources in and a consumer);
are not sufficient to complete all remaining -
subtasks. The execution of never reaches to represent a temporal order between two
an final state: necessary and concurrent tasks, and ;
; - to represent an
- Possible, iff the reachability of a final state is
inhibition of a refinement rule for an
uncertain. According to a particular order of
abstract and necessary task t.
steps firing, a final state may be reached :
- Each transition defined in is a transition
and
or a refinement rule defined in HPlNet.
.
The Petri net defined in the definition 13
constitutes a coordination module including
4. HIERARCHICAL PLANS WITH synchronization constraints that enforce an
SYNCHRONIZATION execution order and ensure the exchange of
some quantities of resources between
4.1. HPlNet with synchronization (SHPlNet) concurrent tasks (explicit positive interaction). It
includes also constraints that enforce the
In this section, we present SHPlNet (Hierarchical selection of one refinement rule.
Plan Net with Synchronization), an extension of
HPlNet [10] that deals with the interaction One can note that several causal relationships
between tasks and plans. can be related to the same resource that is
represented by a unique place. In order to
One can note that the execution of plans may protect the amounts of resources to be
lead to critical situations due to the potential exchanged between different peers of transitions
conflict between the tasks sharing critical (producers and consumers), we propose to add,
resources. The conflict may occur between for each causal relationship, a second temporal
tasks in an individual agent plan or between constraint between the same transitions (using
tasks belonging to different agents' plans. To another place). This additional constraint allows
address these conflicting situations, the tasks in the producer task to notify the availability of
the plans must be synchronized and some expected amount of resource to consumer task.
decomposition methods must be avoided. To be
able to represent plans taking into account the The state of plan represented by SHPlNet is
synchronization between tasks, we extend modeled by the extended marking of SHPlNet
HPlNet by adding features allowing to impose an (definition 14) that takes into account marking
execution order between parallel tasks, and to state of synchronization net.
avoid the activation of some refinement rules.
Definition 14 (extended marking of SHPlNet).
The idea is to add a separate module grouping
synchronization and inhibition constraints. We
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 79
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
An extended marking of SHPlNet firing of refinement rule of a transition that
is defined by the tuple appear in leads to the consumption of tokens.
such that: The production of the tokens will be after the
firing of end transition of the node refining the
- is the extended marking of HPlNet abstract transition (case 3).
; and
- is a marking of ; the initial and the final 4.2. Properties of a SHPlNet
marking of is .
In the same way as a plan represented by
The steps of SHPlNet are firing of an HPlNet, a plan represented by SHPlNet can be
elementary-transition, end-transition, or analyzed from an abstract level. Based on the
refinement-rule. The definition 15 and 16 below summary information about the resources
state respectively the firing condition and firing associated to transitions, we can decide that the
rules. proper termination of plan execution is sure,
Definition 15 (firing condition in SHPlNet). possible, or impossible, provided that this plan is
Given an extended marking , a cycles free. The cycles lead always to deadlock
node in , a step is enabled in state that prevents the execution of any task of
. We formally define the concept of cycle and
, denoted by , iff: acyclic plan as follows.
(i) ;
Definition 17 (Cycle in SHPlNet and Acyclic
(ii) ; Plan).
(iii) . Let be a
In the definition 15, the condition (ii) states that SHPlNet and , be two nodes in .
all possible steps appearing in cannot be includes a cycle represented by
enabled if they are not enabled in . The , iff:
condition (iii) states that an abstract transition (i) for each such that and
appearing in cannot be refined if it is not ,
enabled in . - , or
Definition 16 (firing rules in SHPlNet). - , or
Let be an extended marking, be a - and such that
node in , the firing of a step leads to the , or
extended marking , denoted by - and such that
, if and only iff: .
Case 1: :
(ii) for each such that ,
- ; , and
- ; and
- .
Case 2: :
is called acyclic iff it is cycles free.
- ;
- In the definition 18 we formulate the conditions
, and in which the proper termination of plan execution
- will be sure, possible, or impossible
Case 3: and is child of by 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
+
; and ,
- . - Impossible, iff is is cyclic or
,
In the definition 16 the case 1 states that the - Possible, iff is acyclic and
firing on an elementary transition appearing in and
leads to its firing in . The case 2 states that the
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 80
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
A plan whose execution is impossible is a plan Lemma 5. The proper termination criterion of
that has no way to ensure the success of plan marked SHPlNet is verified
execution. A plan whose the safe execution is if it is quasi-live.
sure is a flexible plan. It can be executed
correctly regardless of the choice to be taken to Proof. To demonstrate that the proper
refine abstract transitions and the execution termination criterion of a SHPlNet is verified if it
order of concurrent tasks. Between these two is quasi-live, we assume that the proper
cases, the success of execution may be termination criterion of a SHPlNet is not verified
possible in an uncertainty case. To address this and demonstrate that it is not quasi-live. We
incertitude, the plan must be reorganized by assume that the termination is not proper. Then,
updating the synchronization net (block some there exists a sink state
refinement rules and/or add some constraints on reachable from the initial state such that .
the execution of tasks). By projecting SHPlNet on HTPN and pursuant to
the theorem 1, if then it must be at least
Soundness of SHPlNet one firable sequence (including steps that are
not yet fired) such that . Thus, if
The consideration of concurrent tasks
synchronization leads to the redefinition of the is sink state then the first step in
conditions under which a hierarchical plan is must be a transition which is enabled vis-a-
sound. Establishing the temporal order vis , but it is not vis-a-vis (or
relationships and exchange of resources ); thus and
between parallel tasks can lead to reduced then is blocking transition. In conclusion,
consumption of resources, which can lead SHPlNet is not quasi-Live. ∎
therefore to obtain a sound plan. However, it
leads to deadlock in cyclic plans. Theorem 4. A marked SHPlNet
is sound if it is quasi-live.
The verification of soundness property of a
SHPlNet is only limited to the verification of Proof. Pursuant to the lemma 4, there is no
quasi-liveness property of all transitions and marked SHPlNet that can
proper termination criterion, because the contain steps to be fired more than once. On the
property relative to the absence of multiple firing other hand, pursuant to the Lemma 5, proper
of steps is inherited directly from HPlNet model. termination criterion is verified if a marked
SHPlNet is quasi-live. Therefore, the marked
Lemma 4. A marked SHPlNet
SHPlNet is sound if it is
does not contain steps that
quasi-live. ∎
can be fired more than once.
In the previous section, we showed how to verify
Proof. By contradiction, we assume that there is
the soundness of a plan represented by HPlNet
(at least) a step that can be fired more than
by analyzing only the summary information
once. Let be step such that
associated with the task of highest abstraction
and level. The condition used for this is not sufficient
. If can be fired again for the case of SHPlNet due to the possible
then there is occurrence of the cycles causing deadlock
such that situations. Therefore, the absence of cycles in a
. By definition plan represented by SHPlNet is a necessary
condition for it to be sound.
implies , and if
which implies
than , and therefore
5. CONCLUSION
. Thus, cannot be fired The work presented in this paper complement
more than once. ∎ our previous works about the representation of
Pursuant to the lemma 4, we can decide that hierarchical plans with synchronization. We
SHPlNet is sound if it is quasi-live and proper presented here a theoretical framework for the
termination criterion is verified. In fact, there is a verification and validation of soundness and
dependency between these two criteria. Each invalidity properties of partial hierarchical plans
termination of SHPlNet, that is not proper, is represented by SHPlNet. We are focused on the
termination when there are steps (exactly demonstration of some key properties that allow
transitions) which cannot be fired, i.e. blocking. to verify the soundness and invalidity of plans by
only analyzing the summary information
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 81
ICAASE'2014 Validation and Verification of Agent andMmulti-Agent Plans in Dynamic Environment
associated to the task of highest abstraction [10] S.Brahimi, R. Maamri, & Z. Sahnoun.
level. "Partially Centralized Hierarchical Plans
Merging". In Recent Developments in
Future work will focus on the analysis of the Computational Collective Intelligence (pp.
computational complexity. We will show how the 59-68). Springer International Publishing,
summary information based analysis can reduce 2014.
the computational complexity compared to the
reachability graph analysis. [11] S.Brahimi, R. Maamri, & Z. Sahnoun.
"Hierarchical Multi-Agent Plans Using
Model-Based Petri Net". International
6. REFERENCES Journal of Agent Technologies and
Systems. (IJATS), 5(2): 1-30. 2013.
[1] Aamodt, Agnar, and Enric Plaza. "Case-
[12] Ziparo, Vittorio Amos, and Luca Iocchi.
based reasoning: Foundational issues,
"Petri net plans." Proceedings of Fourth
methodological variations, and system
International Workshop on Modelling of
approaches". AI communications 7.1 (1994):
Objects, Components, and Agents. 2006.
39-59.
[13] Shaw, P. H., & Bordini, R. H. "Towards
[2] C. Linqin, M. Tao , S.Yining, S. Lei, M.
alternative approaches to reasoning about
Zuchang. "Modeling and analyzing multi-
goals". In Declarative Agent Languages and
agent task plans for intelligent virtual training
Technologies V(pp. 104-121). Springer
system using Petri nets". Sixth World
Berlin Heidelberg. 2008.
Congress on Intelligent Control and
Automation, 2006. The. Vol. 1. IEEE, 2006.
[3] B. J. Clement, E. H. Durfee, and A. C.
Barrett. "Abstract reasoning for planning and
coordination". JOURNAL OF AI
RESEARCH, 28 :453–515, 2007.
[4] K. Erol. Hierarchical Task Network Planning.
Formalization, Analysis, and
Implementation. PhD thesis, College Park,
MD, USA, UMI Order No. GAX96-22054,
1996.
[5] Fallah-Seghrouchni, A. E., Irene
Degirmenciyan-Cartault, and Frédéric Marc.
"Modelling, control and validation of multi-
agent plans in dynamic
context."Autonomous Agents and Multiagent
Systems, 2004. Proceedings of the Third
International Joint Conference on. IEEE,
2004.
[6] Haddad, Serge, and Denis Poitrenaud.
"Recursive petri nets." Acta Informatica44.7-
8: 463-508, 2007.
[7] M. E. Pollack. "The uses of plans". Artificial
Intelligence, 57(1) :43–68, 1992.
[8] Seghrouchni, A. El Fallah, and Serge
Haddad. "A recursive model for distributed
planning." Proceedings of the 2nd
International Conference on Multi-Agent
Systems, 1996.
[9] Christensen, Søren, and Laure Petrucci.
"Modular analysis of Petri nets." The
computer journal 43.3: 224-242. 2000.
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 82