Affiliations: [a] University 8 mai 1945 of Guelma, Guelma, Algeria | [b] University of Constantine 2, Constantine, Algeria
Correspondence:
[*]
Corresponding author: Said Brahimi, University 8 mai 1945 of Guelma, BP 24401, Guelma, Algeria. E-mail: brahimi.said@yahoo.fr.
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
