Linear Completeness Thresholds for Bounded Model Checking.
Bounded model checking is a symbolic bug-finding method that examines paths of bounded length for violations of a given LTL formula. Its rapid adoption in industry owes much to advances in SAT technology over the past 10-15 years. More recently, there have been increasing efforts to apply SAT-based...
| मुख्य लेखकों: | , , , , |
|---|---|
| अन्य लेखक: | |
| स्वरूप: | Journal article |
| भाषा: | English |
| प्रकाशित: |
Springer
2011
|
| _version_ | 1826276833026375680 |
|---|---|
| author | Kroening, D Ouaknine, J Strichman, O Wahl, T Worrell, J |
| author2 | Gopalakrishnan, G |
| author_facet | Gopalakrishnan, G Kroening, D Ouaknine, J Strichman, O Wahl, T Worrell, J |
| author_sort | Kroening, D |
| collection | OXFORD |
| description | Bounded model checking is a symbolic bug-finding method that examines paths of bounded length for violations of a given LTL formula. Its rapid adoption in industry owes much to advances in SAT technology over the past 10-15 years. More recently, there have been increasing efforts to apply SAT-based methods to unbounded model checking. One such approach is based on computing a completeness threshold: a bound k such that, if no counterexample of length k or less to a given LTL formula is found, then the formula in fact holds over all infinite paths in the model. The key challenge lies in determining sufficiently small completeness thresholds. In this paper, we show that if the Büchi automaton associated with an LTL formula is cliquey, i.e., can be decomposed into clique-shaped strongly connected components, then the associated completeness threshold is linear in the recurrence diameter of the Kripke model under consideration. We moreover establish that all unary temporal logic formulas give rise to cliquey automata, and observe that this group includes a vast range of specifications used in practice, considerably strengthening earlier results, which report manageable thresholds only for elementary formulas of the form Fp and Gq . © 2011 Springer-Verlag. |
| first_indexed | 2024-03-06T23:19:46Z |
| format | Journal article |
| id | oxford-uuid:685726ae-19f7-4c9a-a0db-3d08472f6c35 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T23:19:46Z |
| publishDate | 2011 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:685726ae-19f7-4c9a-a0db-3d08472f6c352022-03-26T18:44:12ZLinear Completeness Thresholds for Bounded Model Checking.Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:685726ae-19f7-4c9a-a0db-3d08472f6c35EnglishSymplectic Elements at OxfordSpringer2011Kroening, DOuaknine, JStrichman, OWahl, TWorrell, JGopalakrishnan, GQadeer, SBounded model checking is a symbolic bug-finding method that examines paths of bounded length for violations of a given LTL formula. Its rapid adoption in industry owes much to advances in SAT technology over the past 10-15 years. More recently, there have been increasing efforts to apply SAT-based methods to unbounded model checking. One such approach is based on computing a completeness threshold: a bound k such that, if no counterexample of length k or less to a given LTL formula is found, then the formula in fact holds over all infinite paths in the model. The key challenge lies in determining sufficiently small completeness thresholds. In this paper, we show that if the Büchi automaton associated with an LTL formula is cliquey, i.e., can be decomposed into clique-shaped strongly connected components, then the associated completeness threshold is linear in the recurrence diameter of the Kripke model under consideration. We moreover establish that all unary temporal logic formulas give rise to cliquey automata, and observe that this group includes a vast range of specifications used in practice, considerably strengthening earlier results, which report manageable thresholds only for elementary formulas of the form Fp and Gq . © 2011 Springer-Verlag. |
| spellingShingle | Kroening, D Ouaknine, J Strichman, O Wahl, T Worrell, J Linear Completeness Thresholds for Bounded Model Checking. |
| title | Linear Completeness Thresholds for Bounded Model Checking. |
| title_full | Linear Completeness Thresholds for Bounded Model Checking. |
| title_fullStr | Linear Completeness Thresholds for Bounded Model Checking. |
| title_full_unstemmed | Linear Completeness Thresholds for Bounded Model Checking. |
| title_short | Linear Completeness Thresholds for Bounded Model Checking. |
| title_sort | linear completeness thresholds for bounded model checking |
| work_keys_str_mv | AT kroeningd linearcompletenessthresholdsforboundedmodelchecking AT ouakninej linearcompletenessthresholdsforboundedmodelchecking AT strichmano linearcompletenessthresholdsforboundedmodelchecking AT wahlt linearcompletenessthresholdsforboundedmodelchecking AT worrellj linearcompletenessthresholdsforboundedmodelchecking |