High Level Petri Nets Analysis with Helena

This paper presents the high level Petri nets analyzer Helena. Helena can be used for the on-the-fly verification of state properties, i.e., properties that must hold in all the reachable states of the system, and deadlock freeness. Some features of Helena make it particularly efficient of memory management. Structural abstractions techniques, mainly transitions agglomerations, are used to tackle the state explosion problem. Benchmarks are presented which compare our tool to Maria. Helena is developed in portable Ada and is freely available under the conditions of the GNU General Public License.

• Type: Conference
• Year: 2005
• Where: APN
• Authors: Sami Evangelista
• Keywords: APN 2005, Artificial Intelligence, GNU General Public License, Nets Analyzer Helena, Structural Abstractions Techniques