Publications

Symbolic model checking of multi-modal logics: uniform strategies and rich explanations

Authors
Simon Busard
Tags
, ,
Title
Symbolic model checking of multi-modal logics: uniform strategies and rich explanations
Authors
Simon Busard
sbusard-thesis.pdf Δ   1,716Kb   28 May 2020
Type
Book
Volume
610
Publisher
Doctoral thesis, Université catholique de Louvain
Year
2017

Abstract

Model checking is a verification technique that performs an exhaustive search among the states of safety-critical systems to check whether a given property is satisfied. These properties are usually expressed within a logic that captures different aspects of the system such as its evolution through time.

Multi-modal logics mix several aspects of the system such as the knowledge and strategies of its agents. They usually are branching logics, that is, they can express properties about several successors of the states of interest. Nevertheless, logics to reason about the strategies of agents with an imperfect view of a system under fairness constraints have been seldom considered, and model-checking algorithms appeared only recently.

In this thesis, we first define ATLK_irF, a multi-modal logic reasoning about time, knowledge and uniform strategies of concurrent agents under unconditional fairness constraints. This logic can be used to reason about multi-agent programs under the supervision of a fair scheduler.

We then describe three approaches to solve its model-checking problem. They are all based on an explicit enumeration of the strategies. The first one simply enumerates and checks all uniform strategies of the agents. The second one limits this enumeration to partial strategies, and uses early termination and caching to improve its performances in practice. The last one performs a backward exploration of the system to directly build the winning strategies. Furthermore, we present variants of these approaches based on pre-filtering losing moves. Finally, we implement and compare them with state-of-the-art symbolic solutions. The experiments show that the different approaches outperform the others in different situations.

Second, we attack the problem of generating and manipulating rich explanations for multi-modal logics. One of the main advantages of model checking is its capability to produce a counter-example showing why the checked property is violated. But multi-modal logics have rich and complex explanations, and state-of-the-art model checkers such as NuSMV provide only partial explanations.

We thus present a μ-calculus based model-checking framework. The propositional μ-calculus is a logic integrating modal operators and least and greatest fixpoint operators. The goal of this framework is to help a designer to solve her top-level model-checking problem by translating it into μ-calculus. It integrates a μ-calculus model checker with rich explanations. It also integrates a set of functionalities to help the designer to translate these explanations back into the top-level language, such as formula aliases, a relational graph algebra, and choosers to guide the generation process. The framework is then used on the case of ATL, the standard logic to reason about the strategies of the agents of a system, to show its applicability.

Tags Tags: , ,

BibTeX Record
  @BOOK{lvl-2017-675896,
    TITLE = {Symbolic model checking of multi-modal logics: uniform strategies and rich explanations},
    AUTHOR = {Simon Busard},
    YEAR = {2017},
    VOLUME = {610},
    PUBLISHER = {Doctoral thesis, Université catholique de Louvain},
    URL = {https://lvl.info.ucl.ac.be/Publications/SymbolicModelCheckingOfMulti-modalLogicsUniformStrategiesAndRichExplanations},
  }