In: Lecture Notes in Computer Science, Vol. 1662: Parallel Computing Technologies, pages 134-140. Springer-Verlag, 1997.
Abstract: The intention of this paper is to develop an algorithm for timing behavior analysis of concurrent and real-time systems. The this aim, a notion of parametric time net is introduced which is a modification of time Petri net by using parameter variables in specification of timing constraints on transition firings. A property of the system is given as a formula of parametric TCTL (PTCTL), a real-time branching time temporal logic with timing parameter variables in its operators. Timing behavior analysis consists of finding necessary and sufficient conditions on parameter values under which the checked PTCTL-formula is valid in the given system. Thus the approach allows `mutual adjustment' of timing specifications of both the system and the property via a single execution of verification procedure. The correctness of the proposed algorithm is demonstrated and its complexity is evaluated.
Keywords: PTCTL, branching time temporal logics, concurrent systems, parametric TCTL, parametric behavior, real-time systems, time Petri nets.