License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.175
URN: urn:nbn:de:0030-drops-54147
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5414/
Go to the corresponding LIPIcs Volume Portal

Kupferman, Orna ; Vardi, Gal

On Relative and Probabilistic Finite Counterability

pdf-format:
11.pdf (0.5 MB)

Abstract

A counterexample to the satisfaction of a linear property psi in a system S is an infinite computation of S that violates psi. Counterexamples are of great help in detecting design errors and in modeling methodologies such as CEGAR. When psi is a safety property, a counterexample to its satisfaction need not be infinite. Rather, it is a bad-prefix for psi: a finite word all whose extensions violate psi. The existence of finite counterexamples is very helpful in practice. Liveness properties do not have bad-prefixes and thus do not have finite counterexamples.

We extend the notion of finite counterexamples to non-safety properties. We study counterable languages - ones that have at least one bad-prefix. Thus, a language is counterable iff it is not liveness. Three natural problems arise: (1) Given a language, decide whether it is counterable, (2) study the length of minimal bad-prefixes for counterable languages, and (3) develop algorithms for detecting bad-prefixes for counterable languages. We solve the problems for languages given by means of LTL formulas or nondeterministic Büchi automata. In particular, our EXPSPACE-completeness proof for the problem of deciding whether a given LTL formula is counterable, and hence also for deciding whether it is liveness, settles a long-standing open problem.

We also make finite counterexamples more relevant and helpful by introducing two variants of the traditional definition of bad-prefixes. The first adds a probabilistic component to the definition. There, a prefix is bad if almost all its extensions violate the property. The second makes it relative to the system. There, a prefix is bad if all its extensions in the system violate the property. We also study the combination of the probabilistic and relative variants. Our framework suggests new variants also of safety and liveness languages. We solve the above three problems for the different variants. Interestingly, the probabilistic variant not only increases the chances to return finite counterexamples, but also makes the solution of the three problems exponentially easier.

BibTeX - Entry

@InProceedings{kupferman_et_al:LIPIcs:2015:5414,
  author =	{Orna Kupferman and Gal Vardi},
  title =	{{On Relative and Probabilistic Finite Counterability}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{175--192},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5414},
  URN =		{urn:nbn:de:0030-drops-54147},
  doi =		{10.4230/LIPIcs.CSL.2015.175},
  annote =	{Keywords: Model Checking, Counterexamples, Safety, Liveness, Probability, omega-Regular Languages}
}

Keywords: Model Checking, Counterexamples, Safety, Liveness, Probability, omega-Regular Languages
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI