zbMATH — the first resource for mathematics

SAT-based unbounded model checking of timed automata. (English) Zbl 1159.68480
Summary: We present an improvement to the SAT-based Unbounded Model Checking algorithm K. L. McMillan [Lect. Notes Comput. Sci. 2404, 250–264 (2002; Zbl 1010.68509)]. Our idea consists in building blocking clauses of literals corresponding not only to propositional variables encoding states, but also to more general subformulas over these variables encoding sets of states. This way our approach alleviates an exponential blow-up in the number of blocking clauses. A hybrid algorithm for verifying Timed Automata is proposed, where the timed part of blocking clauses is computed using difference bound matrices. The optimization results in a considerable reduction in the size and the number of generated blocking clauses, thus improving the overall performance. This is shown on the standard benchmark of Fischer’s mutual exclusion protocol.
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Uppaal2k; VerICS