First International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2007) (VECOS)
Verification and Evaluation of Computer and Communication Systems
5-6 May 2007
In this paper, we consider the time Petri net model (TPN model) and show how to detect zenoness using the state class method. Zenoness is a situation which suggests that an infinity of actions may take place in a finite amount of time. This behavior is often considered as pathological since it violates a fundamental requirement for timed systems for they cannot be infinitely fast. Models violating this property are called zeno. We state a necessary and sufficient condition for T-safe TPNs to be zeno and derive an algorithm to verify zenoness in the case of bounded TPN models. We also adapt a model checking approach to verify on-the-fly a subset of TCTL properties while taking into account zeno behaviors.