Integer Reset Timed Automata: Clock Reduction and Determinizability

2010/01/08 by Manasa, Lakshmi, S, Krishna.
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL)

paper · doi:10.48550/arxiv.1001.1215

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.

Related

• On Decidability Timed Automata with 2 Parametric Clocks
• Determinisability of one-clock timed automata
• Reducing Clocks in Timed Automata while Preserving Bisimulation
• Alternating Timed Automata
• New Insights into the Decidability of Opacity in Timed Automata