Page d'accueil du CNRS Page d'accueil de l'Université Paris Diderot Page d'accueil du LIAFA
Laboratoire d'Informatique Algorithmique: Fondements et Applications
CNRS et Université Paris Diderot
UMR 7089
   Staff      Contact      How to get to LIAFA      Teaching      Webmail   

Version française

Page d'accueil de la Fédération de Recherche en Mathématiques de Paris Centre

Page d'accueil de la Fondation Sciences Mathématiques de Paris

Page d'accueil de Sciences En Marche

  • Date: 2009-04-27 [11h]
  • Author: Serge Haddad (LSV)
  • Title: Interrupt Timed Automata
  • Summary:
  • 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 decidable. More precisely we show that the untimed language of an ITA is effectively regular via a generalized class graph. We establish that the reachability problem for ITA is in 2-NEXPTIME and in NP when the number of clocks is fixed. To prove the results on reachability, we first 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). Then we prove that any ITA can be reduced to an equivalent ITA- w.r.t. the language equivalence. Additionally we show that the languages of ITA are neither closed under complementation nor under intersection. We also compare the expressive power of TA and ITA and prove that the corresponding families of languages are incomparable. The result also holds for languages accepted by controlled real-time automata (CRTA), another extension of timed automata. So, we finally combine ITA with CRTA in a model which encompasses both classes and show that the reachability problem is still decidable. This is joint work with B. Bérard

 ©  LIAFA 1995, Last updating: 2016, January webmestre[at]