Date
2009
Titre de la collection
Lecture Notes in Computer Science
n° dans la collection
5504
Indexation documentaire
Informatique générale
Subject
hybrid automata; timed automata; multi-task systems; interruptions; decidability of reachability
Titre du colloque
12th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2009)
Date du colloque
03-2009
Ville du colloque
York
Pays du colloque
Royaume-Uni
Titre de l'ouvrage
Foundations of Software Science and Computational Structures 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings
Auteur
de Alfaro, Luca
Nom de l'éditeur
Springer
Ville de l'éditeur
Berlin
Année
2009
Nombre total de pages
471
ISBN
978-3-642-00595-4
Auteur
Bérard, Béatrice
Haddad, Serge
Type
Communication / Conférence
Nombre de pages du document
197-211
Résumé en anglais
In this work, we introduce the class of Interrupt Timed Automata (ITA), which are well suited to the description of multi-task systems with interruptions in a single processor environment. This model
is a subclass of hybrid automata. While reachability is undecidable for
hybrid automata we show that in ITA the reachability problem is in 2-
EXPSPACE and in PSPACE when the number of clocks is fixed, with a
procedure based on a generalized class graph. Furthermore we consider
a subclass ITA− which still describes usual interrupt systems and for
which the reachability problem is in NEXPTIME and in NP when the
number of clocks is fixed (without any class graph). There exist languages
accepted by an ITA− but neither by timed automata nor by controlled
real-time automata (CRTA), another extension of timed automata. However we conjecture that CRTA is not contained in ITA. So, we combine
ITA with CRTA in a model which encompasses both classes and show
that the reachability problem is still decidable.
