Xiaoyu Mao* **, Janette Cardoso* and Robert Valette**
*IRIT-UT1/LAAS, Toulouse, France
**LAAS-CNRS, 31077 Toulouse, France
Presented at
Automated Technology for Verification and Analysis:
Third
International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7,
Lecture Notes in Computer Science,
Volume 3707 / 2005, pp.278-292
Springer-Verlag GmbH
ISBN: 3-540-29209-8
The objective of this paper is to present a new abstract state space for t-time Petri nets which associates with each path in this space a sequence effectively firable in the net. This means that this state space has to exactly (in a quantitative way) define the set of constraints which have to be verified by the firings. After some definitions about the Simple Temporal Networks, the abstract states are defined as well the generation of the abstract space. It is shown that this space does not coincide with the two previously defined spaces (W and A) in TINA.