Producing explanations for rich logics
(2018) 22nd International symposium on formal methods — Location: Oxford (15.July.2018)
Files
No attached file found for this publication.
Details
- Authors
- Abstract
- One of the claimed advantages of model checking is its capability to provide a counter-example explaining why a property is violated by a given system. Nevertheless, branching logics such as Computation Tree Logic and its extensions have complex branching counter-examples, and standard model checkers such as NuSMV do not produce complete counter-examples—that is, counter-examples providing all information needed to understand the verification outcome—and are limited to single executions. Many branching logics can be translated into the µ-calculus. To solve this problem of producing complete and complex counter-examples for branching logics, we propose a µ-calculus-based framework with rich explanations. It integrates a µ-calculus model checker that produces complete explanations, and several functionalities to translate them back to the original logic. In addition to the framework itself, we describe its implementation in Python and illustrate its applicability with Alternating Temporal Logic.
- Affiliations
Citations
Busard, S., & Pecheur, C. (2018). Producing explanations for rich logics. In Havelund K., Roscoe B., de Vink E. e.a. (ed.), Formal methods : lecture notes in computer science (p. p. 129-146). https://doi.org/10.1007/978-3-319-95582-7_8