SAT-based Unbounded Model Checking of Timed Automata

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Penczek, Wojciech | Szreter, Maciej

Affiliations: Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland. penczek@ipipan.waw.pl, mszreter@ipipan.waw.pl

Note: [] Address for correspondence: Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland

Abstract: We present an improvement to the SAT-based Unbounded Model Checking (UMC, for short) algorithm [13]. 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.

Journal: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 425-440, 2008