← All problems
Unverified
Emptiness-checking for 3-clock Timed Automata with additive constraints
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
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?
