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 badprefix 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 badprefixes and thus do not have finite counterexamples.
We extend the notion of finite counterexamples to nonsafety properties. We study counterable languages  ones that have at least one badprefix. 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 badprefixes for counterable languages, and (3) develop algorithms for detecting badprefixes for counterable languages. We solve the problems for languages given by means of LTL formulas or nondeterministic Büchi automata. In particular, our EXPSPACEcompleteness proof for the problem of deciding whether a given LTL formula is counterable, and hence also for deciding whether it is liveness, settles a longstanding open problem.
We also make finite counterexamples more relevant and helpful by introducing two variants of the traditional definition of badprefixes. 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 = {175192},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897903},
ISSN = {18688969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5414},
URN = {urn:nbn:de:0030drops54147},
doi = {10.4230/LIPIcs.CSL.2015.175},
annote = {Keywords: Model Checking, Counterexamples, Safety, Liveness, Probability, omegaRegular Languages}
}
Keywords: 

Model Checking, Counterexamples, Safety, Liveness, Probability, omegaRegular Languages 
Collection: 

24th EACSL Annual Conference on Computer Science Logic (CSL 2015) 
Issue Date: 

2015 
Date of publication: 

07.09.2015 