
Interrupt Timed Automata
Bérard, Béatrice; Haddad, Serge (2009), Interrupt Timed Automata, in de Alfaro, Luca, 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, Springer : Berlin, p. 197-211. http://dx.doi.org/10.1007/978-3-642-00596-1_15
View/ Open
Type
Communication / ConférenceDate
2009Conference title
12th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2009)Conference date
2009-03Conference city
YorkConference country
Royaume-UniBook title
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. ProceedingsBook author
de Alfaro, LucaPublisher
Springer
Series title
Lecture Notes in Computer ScienceSeries number
5504Published in
Berlin
ISBN
978-3-642-00595-4
Number of pages
471Pages
197-211
Publication identifier
Metadata
Show full item recordAbstract (EN)
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.Subjects / Keywords
hybrid automata; timed automata; multi-task systems; interruptions; decidability of reachabilityRelated items
Showing items related by title and author.
-
Roux, Olivier-Henri; Lime, Didier; Haddad, Serge; Cassez, Franck; Bérard, Béatrice (2005) Communication / Conférence
-
Roux, Olivier-Henri; Bérard, Béatrice; Cassez, Franck; Haddad, Serge; Lime, Didier (2005) Communication / Conférence
-
Bouyer, Patricia; Haddad, Serge; Reynier, Pierre-Alain (2006) Communication / Conférence
-
Bouyer, Patricia; Haddad, Serge; Reynier, Pierre-Alain (2006) Communication / Conférence
-
Bouyer, Patricia; Haddad, Serge; Reynier, Pierre-Alain (2008) Article accepté pour publication ou publié