Paper Info
Title
Producing Explanations for Rich Logics.
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 mu-calculus. To solve this problem of producing complete and complex counter-examples for branching logics, we propose a mu-calculus-based framework with rich explanations. It integrates a mu-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.
Year
DOI
Venue
2018
10.1007/978-3-319-95582-7_8
Lecture Notes in Computer Science
Field
DocType
Volume
Computation tree logic,Model checking,Computer science,Theoretical computer science,Temporal logic,Python (programming language),Branching (version control)
Conference
10951
ISSN
Citations 
PageRank 
0302-9743
2
0.38
References 
Authors
15
2
Name
Order
Citations
PageRank
Simon Busard1403.91
Charles Pecheur228428.50