In: Proc. 8th Int. Workshop on Petri Net and Performance Models (PNPM'99), 8-10 October 1999, Zaragoza, Spain, pages 218-227. 1999.
Abstract: In this paper, we consider the problem of checking 1-safe time Petri nets for linear duration properties, which are linear inequalities on integrated durations of system states. By showing that a 1-safe time Petri net satisfies a linear duration property if and only if its integral behavior satisfies the linear duration property, we can give an algorithm that solves the problem based on investigating the integral state space of the 1-safe time Petri net. The algorithm is also improved to avoid exhaustive investigation of the state space.
Keywords: linear duration properties, time Petri nets.