How Hard Is Finding Shortest Counter-Example Lassos in Model Checking?
Modern model checkers help system engineers to pinpoint the reason for the faulty behavior of a system by providing counter-example traces. For finite-state systems and \(\omega \)-regular specifications, they come in the form of lassos. Lassos that are unnecessarily long should be avoided, as they make finding the cause for an error in a trace harder.
We give the first thorough characterization of the computational complexity of finding the shortest and approximately shortest counter-example lassos in model checking for the full class of \(\omega \)-regular specifications. We show how to build (potentially exponentially larger) tight automata for arbitrary \(\omega \)-regular specifications, which can be used to reduce finding shortest counter-example lassos for some finite-state system to finding a shortest accepting lasso in a (product) Büchi automaton. We then show that even approximating the size of the shortest counter-example lasso is an NP-hard problem for any polynomial approximation function, which demonstrates the hardness of obtaining short counter-examples in practical model checking. Minimizing only the length of the lasso cycle is however possible in polynomial time for a fixed but arbitrary upper limit on the size of strongly connected components in specification automata.
- 3.Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: 32nd Conference on Design Automation (DAC), pp. 427–432. ACM Press (1995)Google Scholar
- 4.De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: 23rd International Joint Conference on Artificial Intelligence (IJCAI), pp. 854–860. IJCAI/AAAI (2013)Google Scholar
- 7.Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems. Springer, Heidelberg (2006)Google Scholar
- 9.Farzan, A., Chen, Y.-F., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2–17. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_2CrossRefzbMATHGoogle Scholar
- 15.Maidl, M.: The common fragment of CTL and LTL. In: 41st Annual Symposium on Foundations of Computer Science (FOCS), pp. 643–652 (2000)Google Scholar
- 19.Sebastiani, R., Tonetta, S.: “more deterministic” vs. “smaller” Büchi automata for efficient LTL model checking. In: 12th IFIP WG 10.5 Advanced Research Working Conference (CHARME), Correct Hardware Design and Verification Methods, pp. 126–140 (2003)Google Scholar