Integration of TChecker in Spot

From LRDE

Revision as of 18:07, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Arthur Remaud | title = Integration of TChecker in Spot | year = 2017 | number = 1712 | abstract = A timed automaton is an <math>\omega</math>-automato...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

A timed automaton is an Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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.