Interrupt Timed Automata with Auxiliary Clocks and Parameters*

Issue title: Reachability Problems for Infinite State Systems

Guest editors: Parosh Aziz Abdulla, Stéphane Demri, Alain Finkel, Jérôme Leroux and Igor Potapov

Article type: Research Article

Authors: Bérard, Beatrice^{a; †} | Haddad, Serge^b | Jovanović, Aleksandra^c | Lime, Didier^d

Affiliations: [a] Sorbonne Université, UPMC-Paris 6, CNRS UMR 7606, Paris, France. Beatrice.Berard@lip6.fr | [b] ENS Cachan, LSV, CNRS, INRIA, Cachan, France. haddad@lsv.ens-cachan.fr | [c] Department of Computer Science, University of Oxford, Oxford, UK. Aleksandra.Jovanovic@cs.ox.ac.uk | [d] École Centrale de Nantes, IRCCyN, CNRS, Nantes, France. Didier.Lime@ec-nantes.fr

Correspondence: [†] Address for correspondence: Sorbonne Université, UPMC-Paris 6, CNRS UMR 7606, Paris, France

Note: [*] This work has been supported by projects ImpRo ANR-2010-BLAN-0317 and PACS ANR-14-CE28-0002

Abstract: Interrupt Timed Automata (ITA) are an expressive timed model, introduced to take into account interruptions according to levels. Due to this feature, this formalism is incomparable with Timed Automata. However several decidability results related to reachability and model checking have been obtained. We add auxiliary clocks to ITA, thereby extending its expressive power while preserving decidability of reachability. Moreover, we define a parametrized version of ITA, with polynomials of parameters appearing in guards and updates. While parametric reasoning is particularly relevant for timed models, it very often leads to undecidability results. We prove that various reachability problems, including robust reachability, are decidable for this model, and we give complexity upper bounds for a fixed or variable number of clocks, levels and parameters.

DOI: 10.3233/FI-2016-1313

Journal: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 235-259, 2016