Interrupt Timed Automata with Auxiliary Clocks and Parameters

TL;DR

This paper extends Interrupt Timed Automata with auxiliary clocks and parameters, maintaining decidability of reachability and providing complexity bounds, thus enhancing the model's expressive power for timed systems.

Contribution

It introduces auxiliary clocks and parametric features to ITA, preserving decidability and enabling more expressive timed system modeling.

Findings

Decidability of reachability is preserved with auxiliary clocks.

Parametric ITA reachability problems are decidable.

Complexity bounds are established for various configurations.

Abstract

Interrupt Timed Automata (ITA) is 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.