Sciweavers

ACSD
2007
IEEE

SAT-based Unbounded Model Checking of Timed Automata

14 years 16 hour ago
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...
Wojciech Penczek, Maciej Szreter
Added 18 Oct 2010
Updated 18 Oct 2010
Type Conference
Year 2007
Where ACSD
Authors Wojciech Penczek, Maciej Szreter
Comments (0)