# Effective Definability of the Reachability Relation in Timed Automata

## TL;DR

This paper presents a new proof demonstrating that the reachability relation in timed automata can be defined using linear arithmetic, simplifying understanding and analysis of such systems.

## Contribution

The paper provides a novel proof of the definability of the reachability relation in timed automata within linear arithmetic, building on prior work.

## Key findings

- Reachability relation is definable in linear arithmetic
- New proof simplifies previous understanding
- Supports automated analysis of timed automata

## Abstract

We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.