Rich Counter-Examples for Temporal-Epistemic Logic Model Checking

Details Rich Counter-Examples for Temporal-Epistemic Logic Model Checking Rich Counter-Examples for Temporal-Epistemic Logic Model Checking

2012-02-21

arxiv.org/abs/1202.4509v1

EPTCS 78, 2012, pp. 39-53

Computer Science

Logic in Computer Science

In Proceedings IWIGP 2012, arXiv:1202.4229

Scientific paper

10.4204/EPTCS.78.4

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.

Affiliated with

Also associated with

No associations

Rating

Rich Counter-Examples for Temporal-Epistemic Logic Model Checking does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Rich Counter-Examples for Temporal-Epistemic Logic Model Checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Rich Counter-Examples for Temporal-Epistemic Logic Model Checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-422408