# Revisiting Reachability in Timed Automata

## TL;DR

This paper provides a simplified proof of the definability of reachability in timed automata, introduces an exponential-space model checking procedure for parametric TCTL, and establishes NEXPTIME-hardness.

## Contribution

It offers a new, simpler proof of a fundamental reachability result and develops an exponential-space model checking method for parametric TCTL.

## Key findings

- Simplified proof of reachability definability in timed automata
- Exponential-space procedure for parametric TCTL model checking
- NEXPTIME-hardness of the reachability fragment of parametric TCTL

## Abstract

We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a new and simpler proof of this result, building on the well-known reachability analysis of timed automata involving difference bound matrices. Using this new proof, we give an exponential-space procedure for model checking the reachability fragment of the logic parametric TCTL. Finally we show that the latter problem is NEXPTIME-hard.