Corrections to A Menagerie of Timed Automata

TL;DR

This paper corrects a technical error in a previous survey regarding the expressiveness of different classes of timed automata, providing corrected constructions and reproofs.

Contribution

It offers corrected constructions and reproofs for the expressiveness equivalence between timed automata with urgent locations and those with false location invariants.

Findings

Corrected the flawed constructions from the original survey.

Reproved the expressiveness equivalence between the two classes of timed automata.

Ensured accuracy of the results in the original survey.

Abstract

This note corrects a technical error in the ACM Computing Surveys paper mentioned in the title. The flaw involved constructions for showing that timed automata with urgent locations have the same expressiveness as timed automata that allow false location invariants. Corrected con- structions are presented in this note, and the affected results are reproved.