Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329792 | Electronic Notes in Theoretical Computer Science | 2005 | 19 Pages |
Abstract
Bounded model checking has until recently been apart from this, typically using a direct conversion from LTL to propositional logic. In this paper we give a new bounded model checking encoding using alternating automata and focus on the relationship between alternating automata and SNF. We also explore the differences in the way SNF, alternating, and Büchi automata are used from both a theoretical and an experimental perspective.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Daniel Sheridan,