Integer Reset Timed Automata: Clock Reduction and Determinizability

TL;DR

This paper introduces a procedure to determinize integer reset timed automata with a single clock, achieving a doubly exponential size bound, and explores subclasses with decidable reachability.

Contribution

It presents a method to produce equivalent deterministic one-clock IRTA with tight size bounds and identifies subclasses with decidable reachability.

Findings

Determinization of IRTA with a doubly exponential size bound.

Tightness of the size bound for the number of locations.

Identification of subclasses of stopwatch automata with decidable reachability.

Abstract

In this paper, we propose a procedure that given an integer reset timed automaton (IRTA) ${\cal A}$, produces a language equivalent deterministic one clock IRTA ${\cal B}$ whose size is at most doubly exponential in the size of ${\cal A}$. We prove that this bound on the number of locations is tight. Further, if integer resets are used in stopwatch automata, a subclass of stopwatch automata which is closed under all boolean operations and for which reachability is decidable is obtained.