Interrupt Timed Automata

Béatrice Bérard 1 Serge Haddad 2
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : 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 2EXPSPACE 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.
Type de document :
Communication dans un congrès
de Alfaro, Luca. 12th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'09), Mar 2009, York, United Kingdom. Springer, Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'09), 5504, pp.197-211, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-00596-1_15〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00772678
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 23:06:43
Dernière modification le : mercredi 21 mars 2018 - 18:58:11

Lien texte intégral

Identifiants

Collections

Citation

Béatrice Bérard, Serge Haddad. Interrupt Timed Automata. de Alfaro, Luca. 12th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'09), Mar 2009, York, United Kingdom. Springer, Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'09), 5504, pp.197-211, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-00596-1_15〉. 〈hal-00772678〉

Partager

Métriques

Consultations de la notice

255