Model Checking Time Petri Nets using NuSMV

Andrea Bobbio, András Horváth

Abstract:

Time Petri Nets (TPN) are Petri Net based models augmented with timing information by associating an interval to each transition. The firing time of a transition is chosen non-deterministically (but not in a stochastic manner) from its associated interval. This paper presents a technique to check if a TPN satisfies temporal properties expressed in real-time Computational Tree Logic (RTCTL). The transition graph of the TPN is built in a compositional manner based on discretization of the firing intervals. The compositional description can be automatically translated into the model description language of NuSMV, a tool for model checking finite state systems against specifications in RTCTL.

Postscript

[Publications of András Horváth]