Integration of TChecker in Spot
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- Authors
- Arthur Remaud
- Type
- techreport
- Year
- 2017
- Number
- 1712
Abstract
A timed automaton is an -automaton which describe a model containing continue time conditions. Without treatments, those automata can have an infinite states space. However, we can translate them in finite automatacalled zone graph, to analyze their properties. In this report, we show how the timed automata have been integrated at Spot. We use TChecker, a program created at the LaBRI. We explain then how we integrate the representation of those TChecker's zone graph in Spot. Then we show how Spot's algorithms can read this translation to work on timed automata and zone graphes. We then explain how inconvenients of TChecker have been adapted to make simpler its utilisation by Spot.
