| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 711388 | IFAC Proceedings Volumes | 2008 | 6 Pages |
Abstract
In this paper, we propose a method for building a Timed Transition Graph (TTG) that uses a single clock from the state class graph of a bounded time Petri Net (TPN). To build this TTG a special state class construction - available in Tina - is used. This structure can be used to calculate “quantitative” temporal properties for the worst case scenario. It is possible to check efficiently several properties over the same TTG if no design modifications are made. Such properties are represented by a framework proposed in the literature were TCTL properties are defined on TPN.
Related Topics
Physical Sciences and Engineering
Engineering
Computational Mechanics
Authors
Pedro M. Gonzalez del Foyo, Jose Reinaldo Silva,