← 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

x+y∼cx + 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?

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu