SAT-based Unbounded Model Checking of Timed Automata

We present an improvement of the SAT-based Unbounded Model Checking (UMC) algorithm. UMC, a symbolic approach introduced in [7], uses propositional formulas in conjunctive normal form (CNF) instead of binary decision diagrams (BDD). The key part of the method consists in elimination of universal quantifiers, where the assignments making a formula non-valid are blocked by blocking clauses. The algorithm suffers from an exponential number of such clauses. Our idea is to allow in blocking clauses literals corresponding not only to variables encoding states, but also to more general subformulas over these variables, thus describing sets of states. A hybrid algorithm is proposed for computing timed part of these clauses, based on the well-known 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 Exclusio...

• Type: Conference
• Year: 2007
• Where: ACSD
• Authors: Wojciech Penczek, Maciej Szreter
• Keywords: ACSD 2007, Clauses Literals, Generated Blocking Clauses, Hardware, SAT-based Unbounded Model