Bounded Model Checking for Weak Alternating Büchi Automata

Reference:

Keijo Heljanko, Tommi Junttila, Misa Keinänen, Martin Lange, and Timo Latvala. Bounded model checking for weak alternating Büchi automata. In Thomas Ball and Robert B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV'2006), volume 4144 of Lecture Notes in Computer Science, pages 95–108, Seattle, WA, USA, August 2006. Springer-Verlag.

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 , where is the size of the initial state predicate, is the bound, is the size of the transition relation, and 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.

Keywords:

Weak Alternating Büchi Automata, Bounded Model Checking, NuSMV, PSL

Suggested BibTeX entry:

@inproceedings{HelJunKeiLanLat:CAV06,
    address = {Seattle, WA, USA},
    author = {Keijo Heljanko and Tommi Junttila and Misa Kein{\"a}nen and Martin Lange and Timo Latvala},
    booktitle = {Proceedings of the 18th International Conference on Computer Aided Verification (CAV'2006)},
    editor = {Thomas Ball and Robert B. Jones},
    month = {August},
    pages = {95--108},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Bounded Model Checking for Weak Alternating {B{\"u}chi} Automata},
    volume = {4144},
    year = {2006},
}

See users.ics.tkk.fi ...