- 109 Downloads
This chapter deals with the timing analysis aspect of the proposed MTG model. This model possesses, next to its behaviour generating aspect, an additional aspect of accepting behaviour. The latter is due to the capturing of various types of timing constraints. Timing analysis answers the question:given a specification S, does it fulfill the set of timing requirements R.
KeywordsMaximum Separation Reachability Graph Operation Node Marked Graph Time Automaton
Unable to display preview. Download preview PDF.
- 16.since the firing moments of a state can be real values, the state space is infinite. In order to be able to perform finite-state verification, we can: (1) restrict the set of values of these firing moments, or (2) group the timed states into a finite number of equivalent state classes. Discrete time verification does the first, while ‘geometric timing analysis’ uses the second (see Section 3.4). The first is justified by the proof that considering only integer event times gives a full characterization of the continuous time behavior for a timed transition system, as proven in [Henzinger 92b].Google Scholar
- 17.i.e. type II & III in his constraint terminology [Vanbekbergen 92, Vanbekbergen 93].Google Scholar
- 25.the model used is Timed Petri nets, as defined by Merlin [Merlin 74].Google Scholar
- 28.i.e. Time Petri nets, as introduced by Merlin [Merlin 74] and consecutively used by Berthomieu [Berthomieu 91]. These time nets have a static time interval associated with each transition.Google Scholar
- 34.i.e. a timed enhanced PN, with transitions carrying a single fixed delays (either deterministic or probabilistic) and relative firing probabilities at choice places [Valette 91].Google Scholar
- 60.sometimes called ‘liveness bound’ [Valette 91].Google Scholar