# Integration of TChecker in Spot

## Abstract

A timed automaton is an ${\displaystyle \omega }$-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.