Distributed generation of state space for timed Petri nets.

摘要

Development of complex systems is usually preceded by detailed studies of their models. For concurrent systems, Petri nets have proved to be a convenient modeling formalism because of their ability to express concurrency, synchronization, precedence constraints and nondeterminism. Timed Petri nets also take into account the durations of modeled activities, facilitating qualitative as well as quantitative analysis of models. The behavior of Petri nets is represented by their state spaces, which are Markov (or embedded Markov) chains. For large models these state spaces easily exceed the resources of a single computer system. Readily available networks of computers provide an attractive alternative to complex methods of state space reduction or aggregation.; The main objective of this project is to use a cluster of PC's or workstations for the state space generation of timed Petri nets. The distributed algorithm uses a divide and conquer technique: disjoint regions of the state graph are constructed on different machines. On each machine the communication is separated from the computation part, and is performed by two specialized concurrent processes: one receiving, and one sending messages. The implementation is based on PVM (Parallel Virtual Machine) using a modified version of TPN-tools, a software package for the analysis of timed Petri nets. Experiments performed on a cluster of 32 PC's connected via a 100 Mbps Ethernet show almost linear speedup for some classes of timed Petri nets.