Model Checking Time Petri Nets using NuSMV

Andrea Bobbio, András Horváth


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.


[Publications of András Horváth]

András Horváth, 2008-06-25