Name
Abstract | ||
|---|---|---|
We present an incremental bounded model checking encoding into propositional satisfiability where the property specification is expressed as a weak alternating Büchi automaton (WABA). The encoding is linear in the specification, or, more exactly ${\mathcal O}(\arrowvert I \arrowvert + k \cdot \arrowvert T \arrowvert + k \cdot \arrowvert \delta \arrowvert)$, where $\arrowvert I \arrowvert$ is the size of the initial state predicate, k is the bound, $\arrowvert T \arrowvert$ is the size of the transition relation, and $\arrowvert \delta \arrowvert$ is the size of the WABA transition relation. Minimal length counterexamples can also be found by increasing the encoding size to be quadratic in the number of states in the largest component of the WABA. The proposed encoding can be used to implement more efficient bounded model checking algorithms for ω-regular industrial specification languages such as Accellera's Property Specification Language (PSL). Encouraging experimental results on a prototype implementation are reported. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11817963_12 | CAV |
Keywords | Field | DocType |
property specification,proposed encoding,transition relation,waba transition relation,encoding size,incremental bounded model checking,regular industrial specification language,chi automaton,property specification language,efficient bounded model checking,specification language | Model checking,Computer science,Satisfiability,Algorithm,Propositional calculus,Property Specification Language,Theoretical computer science,Regular language,Counterexample,Büchi automaton,Bounded function | Conference |
Volume | ISSN | ISBN |
4144 | 0302-9743 | 3-540-37406-X |
Citations | PageRank | References |
12 | 0.69 | 15 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Keijo Heljanko | 1 | 751 | 47.90 |
| Tommi Junttila | 2 | 450 | 30.54 |
| Misa Keinänen | 3 | 38 | 3.59 |
| Martin Lange | 4 | 111 | 9.54 |
| Timo Latvala | 5 | 353 | 18.21 |