Verification of Timed Automata via Satisfiability Checking
- Peter Niebert ,
- Moez Mahfoudh ,
- Eugene Asarin ,
- Marius Bozga ,
- Oded Maler ,
- Navendu Jain
7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02) |
In this paper we show how to translate bounded-length verification problems for timed automata into formulae in difference logic, a propositional logic enriched with timing constraints. We describe the principles of a satisfiability checker specialized for this logic that we have implemented and report some preliminary experimental results.