Proof-like Counter-Examples
Arie Gurfinkel and Marsha Chechik
Department of Computer Science,University of Toronto,
Toronto,ON M5S3G4,Canada.
Email:arie,o.edu
Abstract.Counter-examples explain why a desired temporal logic property fails
to hold,and as such considered to be the most uful form of output from model-
checkers.Reported explanations are typically short and described in terms of
states and transitions of the model;as a result,they can be effectively ud for
debugging.However,counter-examples are not available for every CTL property
情五月
and are often inadequate for explaining exactly what the answer means[CLJV02].
In this paper we prent the approach of annotating counter-examples with addi-
tional proof steps.This approach does not sacrifice any of the advantages of tradi-
tional counter-examples,yet allows the ur to understand and navigate through
the counter-example better.We describe our proof system,discuss how to connect
it with counter-example generators,and prent KEGVis–a tool for visualizing
and browsing the annotated counter-examples.
1Introduction
A model-checker can tell the ur not only whether a desired temporal property holds, but also generate a counter-example,explaining the reasons why this property failed.极简简历
Typically,counter-examples are fairly small and are given in terms of states and transi-
tions of the model;thus,they are readily understood by engineers and can be effectively ud for debugging the model.The counter-example generation ability has been one of
the major advantages of model-checking in comparison with other verification methods.
Counter-examples are a form of mathematical proof:to disprove that some prop-
erty holds on all elements of some t,it is sufficient to produce a single element such that holds on.For model-checking,this has two ramifications.First, counter-examples are restricted to universally-quantified formulas,and cond,counter-
examples have been viewed as infinite orfinite paths,starting from the initial state,that illustrate failure of a given property.This notion of path-like counter-examples has been implemented in SMV[McM93,CGMZ95].Yet only a subt of universally-quantified CTL(ACTL),namely ACTL LTL,has linear counter-examples[CLJV02].Recent work by Clarke et.al.[CLJV02]has extended this notion to tree-like counter-examples. This method generates trees instead of paths as counter-examples and is complete for ACTL.For example,a counter-example for,where shaded areas in-dicate which subformula is being disproved,is shown in Figure1.This example is taken from[CLJV02].Note that tree-like counter-examples are fairly hard to understand:dif-ferent parts of the counter-example correspond to different parts of the property;thus,
Fig.1.Counter-example for(from[CLJV02]).
local information is insufficient to understand what each branch is attempting to dis-prove.This makes it difficult to navigate to“interesting”parts of the counter-example, so the ur has to understand the counter-example in its entirety.
The typical approach of existing counter-example generators is to give a complete explanation,if it is available.Yet the model-checker cannot explain why an existential property is fal or why a universal one is true,and gives no feedback to the ur in the cas.Such an explanation would include the entire model!Thus,in general,we say that a counter-example is not available if it is too large to be practical.Certainly,the problem gets even more difficult when temporal quantifiers are ,(is there a reachable state from which holds in all successors?).Counter-example generators, conventional or tree-like,do not give the ur any feedback for such properties,even though counter-examples are available for parts of the formula.
The goals of the work reported in this paper are as follows:(1)to prerve the desired usability aspects of ,their short length and the clo correspondence to the model;(2)to provide some feedback even if in general the counter-example is not available;(3)to help the ur in understanding complex counter-examples.
Our results follow from the primary obrvation that counter-examples are simply proofs by example;yet they are the coarst type of proofs which skips all steps except tho that result in the transition to the next state.Additional proof steps that explain why the model-checker cho this quence of states for prentation can be added as means of annotating the counter-examples.With this approach,short linear counter-examples remain intuitive,but long and bushy counter-examples become significantly easier to understand becau the ur can refer to the proof for the explanation.Further, when counter-examples are not available,they can be replaced by proof obligations which are either discharged by a theorem-prover or taken on faith.For example,if the model-checker determines that a property holds,we(1)show which states are successors of the current state;(2)indicate that holds in the states;and(3)generate a proof obligation that the current state has no additional successors.The ur might check the last claim by using a theorem-prover or simply by eye-balling the model.
我想和你有个家
In this paper we concentrate on the problem of computing witness to existential properties.This problem is dual to the one of computing counter-examples.We choo witness for our prentation becau wefind it more natural to talk about why a property is true as oppod to why a negation of a property is fal[CGMZ95].The rest of this paper is organized as follows:Section2introduces our notation and gives
2
some background on CTL model-checking.Our approach for generating proofs for fair CTL is introduced in Section3.The main contribution of this paper,the generation and browsing of proof-like counter-examples,is discusd and illustrated in Section4.
Our primary goal is not to produce proofs for all possible temporal properties.In that,we differ from the work that us model-checking for proof generation[PZ01,PPZ01, Nam01,TC02].Instead,we concentrate on annotating counter-examples with proof steps. We compare our results with related work in Section5.Section6concludes the paper with the summary of our approach and venues for future work.
2Background
We assume that the reader is familiar with the basics of model checking and CTL;this information is available in[CGP99].Below,we recall some specific concepts andfix the notation.
We u and to reprent True and Fal,respectively.and are the t of boolean values and all natural numbers,respectively.and
are the least and the greatestfixpoints of a function,respectively.
A Kripke structure is a tuple where is a t of states;
is a(total)transition function;is an initial state,is a t of atomic propositions;and is a(total)labeling function.CTL formulas are evaluated over infinite trees of computations produced by.We write to indicate the value of in state of.If is clear from the context,we omit it from our notation. If a formula holds in the initial ,it is considered to hold in the model.
We u,and as our adequate t for CTL[CGP99].The operators are defined as follows:
def.of
def.of
def.of
We also explicitely define the bounded versions of:
def.of扫兴
def.of
Note that
The remaining operators can be computed from the,as shown in[CGP99].灰色头像歌词
A computation of on which all of the given fairness conditions
occur infinitely often is called a fair computation.Model-checking restricted to fair computations of is called fair,and the resulting language is called FCTL.This lan-guage can be obtained by providing a fair version of()as follows:
def.of
Thus,if and only if is a starting state of some fair computation of .Computing in amounts to restricting
successors of to the ones at the start
3此时无声胜有声作文
1
Fig.2.A simple Kripke structure.
-intro one-point rulemissing是什么意思
universal ca splitting
Fig.3.Some axioms of propositional and boolean logic.
of some fair computation,and evaluating using only the successors.Computing is similar:
def.of
def.of
ECTL is the universal fragment of CTL where every path is existentially quantified and negation is restricted to atomic propositions.ACTL is the dual universal fragment of ,only universal quantification is allowed.Their fair counterparts are referred to as FECTL and FACTL,respectively.
In this paper,we u and to stand for arbitrary atomic propositions,and to reprent states,and and to reprent CTL formulas.We also u the notation to express a formula that evaluates to at state and We u
-rule
atomic-rule
Fig.4.Proof rules for non-temporal operators and.
one simply needs to exhibit an element for which holds.Note also we only consider quantification overfinite domains.
In addition,we assume that all axioms of the theory of Kripke structures and the axiomatization of a particular Kripke structure are available.The latter includes statements about’s transition relation and its labeling function.For example, some of the axioms describing the Kripke structure in Figure2are:
The proof rules for non-temporal operators and are shown in Figure4.They follow directly from the definition of the corresponding operators.The-rule in-troduces an existential quantifier,which is typically eliminated by the one-point rule shown in Figure3.
The proof rules for the bounded are given in Figure5and follow directly from the definition of this operator.To derive the rule for the unbounded,we start by noting the monotonicity of:
Proposition1Let,be ECTL formulas and.Then,
Since we assume that the state space isfinite,the rule is actually bi-directional.That is, for a given Kripke structure,there always exists a natural number,which depends on the diameter of the directed graph induced by,such that. The proof rule for the unbounded is given in Figure5.
To complete our proof system,we need tofind a proof rule for.Unfortunately, we cannot proceed in the same manner as before and u the ECTL equivalence
.Doing so would result in a proof system which is not complete,since this proof rule can potentially be applied an infinite number of times.
Instead,note that is the result of evaluating on all infinite paths emanating from the state.Moreover,si
nce we are dealing withfinite state systems, every infinite path can be decompod into afinite(possibly empty)prefix and afinite repeating suffix.Thus,we can decompo into restricted to all non-trivial cycles around,and restricted to all infinite paths that do not contain in the future.
5
A proof rule for is given in Figure5.
Theorem2The proof system for ECTL is sound and complete.
Proof:
The proof of soundness comes from the fact that our proof rules have been derived using defini-tions and equivalences between ECTL operators.
To prove completeness,we show that any valid statement of the form can be proven by afinite number of applications of our proof rules.The proof proceeds on the structure of the formula.A proof sketch follows:
(1)Let be a propositional temporal formula,that is,does not contain and. Each rule given in Figure4re
duces to its subformulas.Thus,the rest of the proof for this ca proceeds by induction on the number of subformulas of.
(2)If in addition to(1),can also contain,can be removed by expanding it using rules for and given in Figure5.
鸡翅尖的做法
(3)If can contain bounded or unbounded,we note that for a given Kripke structure, there exists an equivalent formula in which all unbounded operators are replaced by their bounded versions,reducing the resulting formula to ca(2)considered above.
(4)If can also ,ECTL,the-rule reduces a formula with to two formulas:(a)the one with,handled by the above ca,and(b)a new formula containing ,where the operator is restricted to a subt of the state space which does not contain the current state.Therefore,this rule can only be applied up to times,ensuring that a valid statement can be proven by afinite number of applications of our proof rules.
6
