Chasing the Best Büchi Automata for Nested Depth-first Search Based Model Checking
| Authors | |
|---|---|
| Year of publication | 2014 |
| Type | Article in Proceedings |
| Conference | 11th Summer School on Modelling and Verification of Parallel Processes (MOVEP'14) |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | LTL, Büchi automata, model checking |
| Attached files | |
| Description | The automata-based model checking uses a translation of formulae in Linear Temporal Logic (LTL) into Büchi automata (BA). The performance of the model checkers can be heavily influenced by the BA used. In this paper we discuss several heuristics commonly used to decide which BA should be used for given verification task, suggest a novel heuristic for this problem and finally evaluate the heuristics using common LTL-to-BA translators, model checker Spin and benchmark of real verification tasks. Our evaluation shows that heuristics based only on number of states of BA or the degree of determinism often give wrong answer or are unable to answer. On a concrete example we further demonstrate our suggestion to exploit some partial knowledge about systems to improve our heuristic. |
| Related projects: |