Timed automata are finite-state automata extended with finite real-valued variables called clocks. Timed automata with additive constraints are timed automata extended with atomic clock constraints of the form \[x + y \sim c\] where x and y are clocks, and c is a constant.

The emptiness-checking problem for Timed automata with additive constraints was shown to be undecidable with only 4 clocks, while it is decidable for 2 clocks [Beìrard Duford '00]. However the case of 3 clocks was left open in the paper.

**Question:** Is the emptiness-checking decidable for timed automata with additive
constraints for 3 clocks?