Probabilistic Petri Net and its Logical Semantics

摘要

There are many variants of Petri net at present, and some of them can model system with both function and performance specification, such as stochastic Petri net, and generalized stochastic Petri net. In order to address the issue of modeling system with probabilistic behaviors, a kind of Petri net with probability (probabilistic Petri net, PPN) is proposed in this paper. Then an action-based PCTL is developed to interpret logical semantics for PPN system. The usefulness of PPN system is illustrated by modeling and specifying an elaborate model of travel arrangements workflow.