Fighting the Clocks Explosion
Résumé
In this talk I will survey several heroic as well as pathetic attempts to fight the clock explosion problem, that is, to find ways to scale-up the automated analysis of timed automata beyond toy problems. The survey will be biased toward efforts I was involved in and will include directions such as BDDs and canonical representations, discretization, search-based techniques, SAT and bounded model-checking, abstraction and partial-order methods. I will also explain why I think this battle is important.