Higher-Dimensional Timed Automata

TL;DR

This paper introduces higher-dimensional timed automata, combining concepts from higher-dimensional automata and timed automata, and demonstrates their reachability complexity, solution algorithms, and extensions to hybrid automata.

Contribution

It presents a novel formalism of higher-dimensional timed automata, analyzes their reachability complexity, and proposes tensor product techniques to mitigate state-space explosion.

Findings

Reachability is PSPACE-complete.

Zone-based algorithms can decide reachability.

Tensor products help combat state-space explosion.

Abstract

We introduce a new formalism of higher-dimensional timed automata, based on van Glabbeek's higher-dimensional automata and Alur's timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also show how to use tensor products to combat state-space explosion and how to extend the setting to higher-dimensional hybrid automata.