Publications

Rich Counter-Examples for Temporal-Epistemic Logic Model Checking

Authors
Simon Busard, Charles Pecheur
Tags
, , ,
Title
Rich Counter-Examples for Temporal-Epistemic Logic Model Checking
Authors
Simon Busard, Charles Pecheur
FM2018 Δ   0Kb   28 May 2020
Fmics2013 Δ   0Kb   28 May 2020
GandALF2017 Δ   0Kb   28 May 2020
HMI2011 Δ   0Kb   28 May 2020
LVLPrivate Δ   0Kb   28 May 2020
LVLPrivateNews Δ   0Kb   28 May 2020
Main Δ   0Kb   28 May 2020
Members Δ   0Kb   28 May 2020
Publications Δ   4Kb   28 May 2020
Site Δ   0Kb   28 May 2020
Talks Δ   4Kb   28 May 2020
Tools Δ   0Kb   28 May 2020
Type
In Proceedings
Book title
Proceedings Second International Workshop on Interactions, Games and Protocols, Tallinn, Estonia, 25th March 2012
Series
Electronic Proceedings in Theoretical Computer Science
Volume
78
Pages
39-53
Publisher
Open Publishing Association
Editor
Johannes Reich and Bernd Finkbeiner
Year
2012

Abstract

Model checking verifies that a model of a system satisfies a given property, and otherwise produces a counter-example explaining the violation. The verified properties are formally expressed in temporal logics. Some temporal logics, such as CTL, are branching: they allow to express facts about the whole computation tree of the model, rather than on each single linear computation. This branching aspect is even more critical when dealing with multi-modal logics, i.e. logics expressing facts about systems with several transition relations. A prominent example is CTLK, a logic that reasons about temporal and epistemic properties of multi-agent systems. In general, model checkers produce linear counter-examples for failed properties, composed of a single computation path of the model. But some branching properties are only poorly and partially explained by a linear counter-example.

This paper proposes richer counter-example structures called tree-like annotated counter-examples (TLACEs), for properties in Action-Restricted CTL (ARCTL), an extension of CTL quantifying paths restricted in terms of actions labeling transitions of the model. These counter-examples have a branching structure that supports more complete description of property violations. Elements of these counter-examples are annotated with parts of the property to give a better understanding of their structure. Visualization and browsing of these richer counter-examples become a critical issue, as the number of branches and states can grow exponentially for deeply-nested properties.

This paper formally defines the structure of TLACEs, characterizes adequate counter-examples w.r.t. models and failed properties, and gives a generation algorithm for ARCTL properties. It also illustrates the approach with examples in CTLK, using a reduction of CTLK to ARCTL. The proposed approach has been implemented, first by extending the NuSMV model checker to generate and export branching counter-examples, secondly by providing an interactive graphical interface to visualize and browse them.

Tags Tags: , , ,

BibTeX Record
  @INPROCEEDINGS{lvl-2012-994846,
    TITLE = {Rich Counter-Examples for Temporal-Epistemic Logic Model Checking},
    AUTHOR = {Simon Busard and Charles Pecheur},
    YEAR = {2012},
    VOLUME = {78},
    PAGES =  {39-53},
    PUBLISHER = {Open Publishing Association},
    EDITOR = {Johannes Reich and Bernd Finkbeiner},
    SERIES = {Electronic Proceedings in Theoretical Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/RichCounter-ExamplesForTemporal-EpistemicLogicModelChecking},
  }