=Paper=
{{Paper
|id=Vol-1256/paper3
|storemode=property
|title=Diagnosis of Probabilistic Models using Causality and Regression
|pdfUrl=https://ceur-ws.org/Vol-1256/paper3.pdf
|volume=Vol-1256
|dblpUrl=https://dblp.org/rec/conf/vecos/Debbi14
}}
==Diagnosis of Probabilistic Models using Causality and Regression==
https://ceur-ws.org/Vol-1256/paper3.pdf
34
Diagnosis of Probabilistic Models using
Causality and Regression
Hichem Debbi
Department of Computer Science
University of M’sila
M’sila
Algeria
hichem.debbi@gmail.com
The counterexample in probabilistic model checking (PMC) is a set of paths in which a path formula
holds, and their accumulated probability violates the probability bound. However, understanding the
counterexample is not an easy task. In this paper we address the complementary task of counterexample
generation, which is the counterexample analysis. We propose an aided-diagnostic method for probabilistic
counterexamples based on the notions of causality and regression analysis. Given a counterexample for a
Probabilistic CTL (PCTL)/Continuous Stochastic Logic (CSL) formula that does not hold over Discrete Time
Markov Chain (DTMC)/Continuous Time Markov Logic (CTMC) model, this method generates the causes of
the violation, and describes their contribution to the error in the form of a regression model.
Probabilistic Model Checking (PMC), Probabilistic Computation Tree Logic (PCTL), Probabilistic
Counterexample, Causality, Structural Equation Modeling (SEM), Regression Analysis.
1. INTRODUCTION (2009, 2010, 2011); Han et al. (2009). In PMC, this
task is more challenging.
Probabilistic Model Checking (PMC) has appeared
as an extension of model checking for modelling and Generating small and indicative counterexamples
analysing systems that exhibit stochastic behaviour. only is not enough for understanding the error.
Several case studies in several domains have been Therefore, in conventional model checking, many
addressed from randomized distributed algorithms works have addressed the analysis of counterex-
and network protocols to biological systems and amples to understand the failure (Ball et al. (2003),
cloud computing environments. These systems Zeller et al. (2002), Groce et al. (2003), Groce et al.
are described usually using Discrete-Time Markov (2006), Wang et al. (2006), Kumazawa and Tamai
Chains (DTMC), Continuous-Time Markov Chains (2011), Beer et al. (2011)). As it was done in
(CTMC) or Markov Decision Processes (MDP), and conventional model checking, addressing the error
verified against properties specified in Probabilistic explanation in the PMC is highly required, especially
Computation Tree Logic (PCTL) Hansson and that probabilistic counterexample is a set of multiple
Jonsson (1994) or Continuous Stochastic Logic paths instead of single path, and it is probabilistic.
(CSL) (Aziz et al (2000), Baier et al (2003)).
In this paper, we address the diagnosis of
Unlike the previous methods proposed for conven- probabilistic counterexamples. To this end, we adopt
tional model checking that generate the counterex- the definition of causality based on counterfactuals
ample as a single path ending with bad state repre- by Halpern and Pearl (Halpern and Pearl (2001))
senting the failure, the task in PMC is quite different. to reason formally about the causes, and then
The counterexample in PMC is a set of evidences transform the causality model into regression model
or diagnostic paths that satisfy the formula and their using Structural Equation Modelling (SEM) in order
probability mass violates the probability bound. As to quantify the contribution of these causes to the
it is in conventional model checking, the generated error . SEM is a comprehensive analytical method
counterexample should be small and most indicative used for testing and estimating causal relationships
to be easy for understanding Aljazzar and Leue between variables embedded in theoretical causal
model (Wright and Sewall (1921)). Regression
35
analysis, path analysis and factor analysis are all 2.1. Probabilistic Computation Tree Logic
special cases of SEM. (PCTL)
This paper contains two complementary contribu- The Probabilistic Computation Tree Logic (PCTL)
tions. The first defines a formal causality model for has appeared as an extension of CTL for the
the counterexample, where we give the definition of specification of systems that exhibit stochastic
an actual cause for the violation of PCTL/CSL for- behaviour. We use the PCTL for defining quantitative
mula φ = P≤p (ϕ). The second complements the first properties of DTMCs. PCTL state formulas are
by generating a regression model from the causality formed according to the following grammar:
model, which quantifies the effect of each cause on
the violation of the PCTL/CSL formula. In this paper, φ ::= true|a|¬φ|φ1 ∧ φ2 |P∼p (ϕ)
we will focus on upper bounded properties. Lower
bounded properties can be transformed easily to up- Where a ∈ AP is an atomic proposition, ϕ is a
per bounded properties (Aljazzar and Leue (2010), path formula, P is a probability threshold operator,
Han et al. (2009)). Our approach does not ignore ∼∈ {<, ≤, >, ≥} is a comparison operator, and p
the previous approaches of generating probabilistic is a probability threshold. The path formulas ϕ are
counterexamples, but instead it is based on them. formed according to the following grammar:
Our approach for error explanation is based directly
ϕ ::= φ1 Uφ2 |φ1 Wφ2 |φ1 U≤n φ2 |φ1 W≤n φ2
on the most indicative counterexamples(Aljazzar and
Leue (2010), Han et al. (2009)). Where φ1 andφ2 are state formulas and n ∈ N . As in
CTL, the temporal operators (U for strong until, W for
The rest of this paper is organized as follows.
weak (unless) until and their bounded variants) are
In Section 2, we present some preliminaries
required to be immediately preceded by the operator
and definitions. The Probabilistic Computation Tree
P. The PCTL formula is a state formula, where
Logic (PCTL) and probabilistic counterexamples are
path formulas only occur inside the operator P. The
presented in this section. In section 3, we give the
operator P can be seen as a quantification operator
definition of Causes in probabilistic counterexamples
for both the operators ∀ (universal quantification) and
with the formal causality model, and then we
∃ (existential quantification), since the properties are
show how to generate the regression model from
representing quantitative requirements.
it. Following that, we introduce an algorithm for
generating the causes of violation of PCTL/CSL The semantics of a PCTL formula over a state s (or
properties and the related regression model. Section a path σ) in a DTMC model D = (S, sinit , P, L) can
4 describes an experimental study. Section 5 be defined by a satisfaction relation denoted by |=.
presents the related works. At the end, we present The satisfaction of P∼p (ϕ) on DTMC depends on the
conclusion and future works. probability mass of set of paths satisfying ϕ. This set
is considered as a countable union of cylinder sets,
2. PRELIMINARIES AND DEFINITIONS so that, its measurability is ensured.
A Discrete-Time Markov Chain (DTMC)is a tuple The semantics of PCTL state formulas for DTMC is
D = (S, sinit , P, L) , such that S is a finite set of defined as follows:
states, sinit ∈ S the initial state,P : S × S → [0, 1]
s |= true ⇔ true
represents the transition probability matrix, L : S →
s |= a ⇔ a ∈ L(s)
2AP is a labelling function that assigns to each state
s |= ¬φ ⇔ s 6|= φ
s ∈ S the set L(s) of atomic propositions. An infinite
s |= φ1 ∧ φ2 ⇔ s |= φ1 ∧ s |= φ2
path σ is a sequence of states s0 s1 s2 ... , where
s |= P∼p (ϕ) ⇔ P (s |= ϕ) ∼ p
P (si , si+1 ) > 0 for all i ≥ 0. A finite path is finite
prefix of an infinite path. We define a set of paths Given a path σ = s0 s1 ... in D and an integer j ≥
starting from a state s0 by P aths(s0 ). The underlying 0, where σ[j] = sj , The semantics of PCTL path
σ-algebra is formed by the cylinder sets which are formulas for DTMC is defined as for CTL as follows:
induced by finite paths in P aths(s0 ). The probability
of this cylinder set is: σ |= φ1 Uφ2 ⇔ ∃j ≥ 0.σ [j] |= φ2 ∧ (∀0 ≤ k <
j.σ [k] |= φ1 )
P (σ ∈ P aths(s
Q 0 )|s0 s1 ...sn is a prefix of σ) = σ |= φ1 Wφ2 ⇔ σ |= φ1 Uφ2 ∨ (∀k ≥ 0.σ [k] |= φ1 )
i≤0 P (CX2 ).The strongest path is
terexample M IP CX(s0 |= φ) contains at least one
P (s0 s2 s3 ) = 0.24, which is included in the most
strongest path σ ∈ F initeP aths(s0 |= φ).
indicative probabilistic counterexample.
Lemma 2.2 For every path σ ∈ M IP CX(s0 |= φ)
on which the property φ1 Uφ2
37
2.3. Causality Background in the current context. Minimality condition ensures
→
−
that only elements in the conjunction X = → −x are
Halpern and Pearl (Halpern and Pearl (2001)) have essential for changing ϕ from true to false. As a
extended the Lewis counterfactual model (Lewis consequence of this condition, we can refer to a
(1973)) to what they refer to as structural equations cause as X = x, because the causes can always be
for modelling the causal influence made by random taken to be single conjuncts (Chockler and Halpern
variables. They introduce the causality model M as (2004)).
a tuple M = (U, V, F ), where random variables are
partitioned into two sets, the exogenous variables U , 2.4. Regression Analysis
whose values are determined by factors outside the
model M, but they should be represented to encode Regression analysis is a statistical technique
the context, and the endogenous variables V whose enables us to reason about the relationship between
values are determined by set of functions F , where variables. It describes the change in value of
each fVi ∈ F is a mapping from U ∪ (V \ Vi ) to a variable Y , namely dependent or endogenous
Vi . Thus, each fVi tells us the value of Vi given the in response to the variation of a variable X
values of all other variables in U ∪ V . namely independent or exogenous. The relationship
between these variables is either positive or
We call a Boolean combination of primitive events a negative. If the value of Y increases when the
basic causal formula. We call a Boolean combination value of X rises, it is said that the relationship
of basic causal formulas a causal formula. A causal is positive. Conversely, the relationship is said to
formula ϕ is true or false in causal model, given a be negative. One of the relationships that we can
context. We write (M, →−u ) |= ϕ if ϕ is true in causality infer and statistically reason about using regression
model M given a context → −
u , where → −u represents analysis is causality. The causal model is build
a setting for the variables in U . We write (M, → −u ) |= based on assumptions or hypothesis, and then is
→
− →
− →
−
[ Y ← y ](X = x), where Y ⊂ V , if X has a value tested against statistical data to determine how the
x in M given a context → −u and the assignment → −
y to specified model fits the data. So when it comes to
→
−
Y . The formulas that are allowed to be causes for ϕ causal relationships, we can use regression analysis
are ones of the form X1 = x1 ∧ ... ∧ Xk = xk which to estimate the causal effect instead of exploring
→
−
is abbreviated to the form X = → −x . With all these the causal relationships. The causal relationship
definitions in hand, we can now give the definition of between dependent variable Y and independent
an actual cause by Halpern and Pearl. variable X with the consideration of factors noise
called disturbance term or error term and denoted
→
−
Definition 2.1 (Actual Cause) we say that X = → −
x ε is given by the linear equation
→
−
is an actual cause of ϕ in (M, u ) if the following
holds: Y = βX + ε (1)
→
−
1. (M, →
−
u ) |= ( X = →
−
x)∧ϕ
Where X stands as a cause for Y ,β stands as a
→
− −→ coefficient or weight that quantifies the direct causal
2. There exists a partition ( Z , W ) of V with
→
− →
− effect of X on Y . ε is an error term stands for
X ⊆ Z and some setting (→ −
x 0, →
−
w 0 ) of the
→
− −→ all extraneous variables, which are assumed to be
variables in ( X , W ) such that if uncorrelated with X. Whereas the variables X and
→
−
(M, →−
u ) |= Z h= z ∗ for Z ∈ Z , then Y are perfectly known, the objective behind using
→
− −
→
a-(M, → −u ) |= X ← → −
x 0, W ← → −
i
w 0 ∧ ¬ϕ regression analysis is to produce an estimate of the
b- two parameters β and ε.
h→
− −
→ →
− →
−i
(M, →−
u ) |= X ← → −x,W ← → −
w 0, Z 0 ← z∗ ∧ ϕ
→
− →
−
for all subsets Z 0 of Z . 3. CAUSES IN PROBABILISTIC
→
− COUNTEREXAMPLES
3. The set of variables X is minimal (no subset
→
−
of X satisfies the conditions 1 and 2). For probabilistic properties of the form φ = P6p (ϕ)
, explaining the violation reduces to the explanation
→
−
The first condition states that both X = → −
x and ϕ are of exceeding the probability bound over the DTMC
→
−
true in the current context, given the variables X and model. Therefore, the question:what labelling and/or
→
−
their values x . The second condition states that any probability values in the counterexample causes the
→
− −→ system to falsify a specification, reduces to the
change on ( X , W ) will change ϕ from true to false,
−
→ question: what labelling and/or probability values
changing W will have no effect on ϕ as long as the
→
− in the counterexample causes the exceeding of
values of X are kept at the current values, even if
→
− →
− probability bound over the model.
all subsets Z 0 of Z are set to their original values
38
3.1. Causality Model X
CC σ (X = x) = P (s) (2)
A causality model for the most indicative s∈σ|fX (s)=x
probabilistic counterexample M IP CX(s0 |= φ) is a
tuple M = (U, V, F ), where the set U is represented
That is, with respect to each path σ ∈ M IP CX(s0 |=
by a context variable; its value u represents a state
φ), we have associated to each cause a measure
s ∈M IP CX(s0 |= φ). V is a set of atomic
that represents the sum of probabilities of reaching
propositions and Boolean formulas. F associates
the states in which X = x. We can say that X = x is
with every variable Vi ∈ V a truth function fVi that
a cause for the satisfaction of ϕ with respect to a path
determines the value of Vi (0 or 1), given a state s
σ with a contribution CC σ . So, the cause having the
and the values of other variables in V .
highest contribution will be the one found the most
along the path.
For example, fp∧r (s, p = 1, r = 1) = 1 where p and r
Example. Consider the most indicative counterex-
are atomic propositions, and s is state representing
ample
a context. The causal influence is modelled by the
transitions in M IP CX(s0 |= φ). CX3 =
{s0 s2 s3 , s0 s1 s4 , s0 s2 s4 , s0 s1 s3 , s0 s2 s1 s4 , s0 s1 s2 s3 }
\ 0 ) (s0 |= φ) the set
Let us denote by M IP CX(s,X←x
of finite paths resulted from M IP CX(s0 |= φ) by generated from the DTMC presented in Fig1 against
switching the value of a variable X ∈ V in a state the property P≤0.7 (ϕ), where ϕ = (a ∨ b)U (c ∧ d). It is
s. possible to define a causality model for CX3 , where
u ∈ {s0 , s1 , s2 , s3 , s4 , s5 }, and F can be defined over
Definition 3.2 (Criticality) Consider a the variables in V as follows
counterexample M IP CX(s0 |= φ) for a probabilistic
formula φ = P≤p (ϕ), a state s ∈ M IP CX(s0 |= φ) fa (s1 ) = 1
and a variable X ∈ V has a value x ∈ {0, 1} in s. fc∧d (s1 , c = 0, d = 0) = 0
We say that (X = x) is critical for the violation of ...
\ 0 ) (s0 |= φ) is not a
φ = P≤p (ϕ) in s, if M IP CX(s,X←x
valid counterexample for φ = P≤p (ϕ). For instance, it is clear that in s2 , the actual cause
for the satisfaction of ϕ = (a ∨ b)U (c ∧ d) is b = 1.
That is, for the probabilistic counterexample The probability of the actual cause b = 1 in the path
M IP CX(s0 |= φ), we say that the value of a σ2 = s0 s2 s3 is CC σ2 (b = 1) = 0.6.
variable X is critical for the violation of φ = P≤p (ϕ)
in a state s, if changing the value of X in this state 3.2. Model Analysis
renders the result not a counterexample.
We aim now quantify the effect of a cause X =
x on the violation of φ. To do so, we use the
Definition 3.3. (Actual Cause) Consider a
regression analysis as a comprehensive technique
counterexample M IP CX(s0 |= φ) for a probabilistic
for estimating this effect, where the path formula
formula φ = P≤p (ϕ) and a variable X ∈ V . We say
ϕ will stand as a dependent variable, whereas the
that (X = x) is a cause for the violation of
formula of the form X = x will stand as an
φ = P≤p (ϕ) in s, if (X = x) is critical , or there exists
−
→ independent variable. So, the regression model will
a subset of variables W of V in s such that switching describe the behaviour of the system by analysing
the values →
−
w of W in s makes (X = x) critical. the change of the probability of ϕ satisfaction with
respect to variables that are considered to be
Thus, in our setting, we can refer to a cause as causes.
(X = x) where X is an atomic proposition has the
value 1 in s if X ∈ L(s), and it has the value 0 While the variables are now well defined, the
otherwise. (X = x) is said to be cause in state s, remaining task is to generate the data required for
if it is critical, or it can be made critical by switching estimating the structural parameters. With respect to
the values of set of variables W in s. the definition of diagnostic causality model, we have
seen that each cause X = x has a contribution
Definition 3.4. A Diagnostic causality model for CC σ (X = x) with respect to each path σ ∈
M IP CX(s0 |= φ) is a tuple hM, CC σ i, where M is M IP CX(s0 |= φ). So in our setting, P (σ) will stand
a causality model, and CC σ is a contribution for the value of ϕ and CC σ (X = x) will stand for the
function that assigns to each cause its contribution value of X = x . As a result, the number of data rows
to the satisfaction of ϕ with respect to a path will be exactly the number of finite paths forming
σ ∈ M IP CX(s0 |= φ) as follows the M IP CX(s0 |= φ). We present an algorithm for
39
generating the causes and their contributions, hence end findCauses
constructing the data set.
The algorithm explores the counterexample path by
This algorithm performs on counterexample gener- path, and computes the causes that will act as
ated by the tool DiPro (Aljazzar and Leue (2011)), data variables, and computes their probabilities that
since probabilistic model checkers do not have will act as data values. We notice that these two
the ability to generate counterexamples. DiPro is tasks are performed simultaneously. We compute
a tool used for generating counterexamples from CC σ (X = x) of each cause X = x found in set
DTMC, CTMC and MDPs models, and can be of states. The condition put on last state follows
jointly used with the model checkers PRISM and Lemma 2.3. The main function of this algorithm is
MRMC. The algorithm gets from DiPro tool the FindCauses. It takes a state and state formula as
counterexample M IP CX(s0 |= φ) and the proba- input and returns recursively a set of causes. We
bilistic formula φ = P6p (ϕ) as input, and outputs note that when the state formula ψ is of the form
the dataset. The formula ϕ is until formula of the ψ1 ∧ ψ2 , both sub-formulas are essentially true at
form φ1 Uφ2 (φ1 U≤n φ2 )given in NNF (Negative Nor- state s. But When ψ is of the form ψ1 ∨ ψ2 , one
mal Form). of them could be true at s or both of them. This
actually follows the causal intuition that in conjunctive
Algorithm. ComputeDataset scenario, both ψ1 and ψ2 are required for ψ being
Inputs: The probabilistic formula φ = P≤p (ϕ) satisfied, whereas in the disjunctive scenario, either
The counterexample M IP CX(s0 |= φ) ψ1 or ψ2 suffices to make ψ satisfied. In the two
Outputs: DataSet: Variables (causes) with values (CC σ ) cases, we apply FindCauses to each sub-formula.
begin Finally, at the propositional level, the cause would
Causes := ∅ be a(a = 1) or ¬a(a = 0), and it is allowed to be
for each path σ ∈ M IP CX(s0 |= φ) do a conjunction of primitive formulas.
for each state s ∈ σ do
if s is the last state in σ then The Algorithm over-approximates the set of causes
Causes := findCauses(s, φ2 ) , since computing the set of causes exactly in
CC σ (Causes) = s∈σ|fX (s)=x P (s)
P
binary causal models is NP-complete (Eiter and
end if Lukasiewicz (2002)). In (Beer et al. (2011)), the
else authors introduced a polynomial algorithm that
Causes := findCauses(s, φ1 ) approximates the set of causes for the violation
CC σ (Causes) = s∈σ|fX (s)=x P (s) of LTL formula. The reduction from binary causal
P
end else models to Boolean circuits and from Boolean circuits
end for to model checking as introduced in (Chockler et al.
end for (2007)) proved that computing the causes and the
end ComputeDataset degree of responsibility for branching time formula is
function findCauses(s, ψ) also NP-complete, and they provided a polynomial
begin algorithm for computing responsibility for read-once
if ψ is of the form ψ1 ∧ ψ2 then Boolean formulas.
return findCauses(s, ψ1 ) ∪ findCauses(s, ψ2 )
end if It is evident that the complexity of this algorithm is
If ψ is of the form ψ1 ∨ ψ2 Then polynomial in size of M IP CX(s0 |= φ) and the size
If s |= ψ1 and s |= ψ2 Then of ϕ. This follows from the fact that the left sub-
return FindCauses(s, ψ1 ) ∪ FindCauses(s, ψ2 ) formula φ1 is evaluated in each state except the last
End If ones, in which the right sub-formula φ2 is evaluated,
If s |= ψ1 and s 6|= ψ2 this is much less hard than evaluating both sub-
return FindCauses(s, ψ1 ) formulas at each state of the counterexample (Beer
End If et al. (2011)). Moreover, if the sub-formula is
If s 6|= ψ1 and s |= ψ2 AND formula, it is not necessary to be evaluated,
return FindCauses(s, ψ2 ) since its satisfaction is ensured. Once the causes
End If found in state s, computing the causes probability is
End If performed each time at a state s with respect to each
if ψ is of the form a where a ∈ AP and a ∈ L(s) then path.
return a
3.3. Illustrative Example
end if
if ψ is of the form ¬a where a ∈ AP and a ∈ / L(s) then We modelled the DTMC presented before in Fig.1
return¬a in PRISM. Then we generate most indicative
end if counterexample using DiPro for the property
40
P≤0.7 (ϕ). The counterexample generated is CX3
where
P (CX3 ) =
P ({s0 s2 s3 , s0 s1 s4 , s0 s2 s4 , s0 s1 s3 , s0 s2 s1 s4 , s0 s1 s2 s3 })
= 0.24 + 0.16 + 0.12 + 0.08 + 0.072 + 0.064
We pass the counterexample to be analyzed to our
algorithm, which is implemented in Java. It takes
the counterexample generated by DiPro in XML
Figure 2: Embedded controle system
format and returns the dataset. The set of causes as
can be generated for this counterexample using our
algorithm is as follows:C1 = a, C2 = b, C3 = {c, d} f ail sensors = (i = 2 ∧ s < M IN SEN SORS)
f ail actuators = (o = 2∧a < M IN ACT U AT ORS)
These causes denoted Ci stand as independent
f ail io = (count = M AX COU N T + 1)
variables (X) for the regression model we are going
f ail main = (m = 0)
to build, where the until formula ϕ denoted UF stands
for the dependent variable (Y). The data values We use the variable M ax Count to refer to the
of these observed variables are given in the table maximum number of consecutive cycles skipped
bellow allowed. Thus, the I/O processor will fail if the count
UF C1 C2 C3 exceeds the limit M ax Count. The down status of
the system is labelled as:
0.24 1 0.6 0.24
0.16 1.04 0 0.16 down =
0.12 1 0.6 0.12 f ail sensors|f ail actuators|f ail io|f ail main
0.08 1.04 0 0.08
0.072 1.03 0.6 0.072 That is, the systems is down if any of this failures
0.064 1.04 0.4 0.064 occurs. For this model, we choose the property that
Table 1: CX3 data set estimates the probability of I/O failure occurring first,
which is given as follows:
P =?[¬(down)U f ail io]
As we see in the table, the number of data rows
represents the number of paths of M IP CX(s0 |= φ), We test this property using PRISM for
where the value of until formula UF refers to the (M ax Count = 6). For this value, PRISM renders
probability of each path P (σ) and the value of cause a probability equal to 0.11. We chose the value
refers to CC σ (X = x) . 0.1 as a threshold for this property to generate the
counterexample. Thus the property can be rewritten
4. EXPERIMENTAL RESULTS as follows:
We have implemented the above method in Java. P ≤ 0.1[¬(down)U f ail io]
To evaluate our method, we use two benchmark
case studies, the embedded control systems taken We use DiPro to generate the counterexample,
from (Muppala et al. (1994)) and the cyclic polling which in turn uses PRISM. The counterexample
model taken from (Ib and Trivedi (1990)). All the can be rendered graphically and stored in XML
experiments were carried out on windows XP with format. The tool implements many algorithms. In
Intel Pentium CPU 3.2 GHz speed And 512 mb of our experiments, we used the heuristic search
memory. algorithm XBF that computes the counterexample
as a diagnostic sub-graph. Our method takes the
4.1. Embedded Control System counterexample generated from DiPro in XML format
and the property to be verified , and outputs the
The system consists of input processor (I) that reads causes and their values as a dataset in Excel file.
incoming data from three sensors (s1,s2,s3) and This excel file is passed to the tool AMOS in order
then passes it to main processor (M). The processor to generate the regression model. AMOS is well-
M processes the data and sends instructions to an known software for SEM that enables user to specify,
output processor (O) that controls two actuators (A1 confirm and refine models, by incorporating many
and A2) using these instructions.Any of the system’s statistical methods.
components M, I/O, the sensors and the actuators
may fail; as a result the system is shut down. The
types of failure are:
41
What concerns us more, is how to get the
diagnostic information by interpreting these weights
or coefficients. We should recall that C1(input
processor is not in OK state),C2(all sensors are
working) are the probable causes for not sensor
failure occurring, whereas C3(output processor is not
in OK state),C4 (all actuators are working) are the
causes for not actuators failure occurring. Here we
Figure 3: Regression weights are facing a disjunctive scenario for both failures.
In fact, the weights presented above have more
importance when we face a disjunctive scenario
The PRISM model consists of 6858 states and (ψ1 ∨ ψ2 ), because the designer will need to know
28907 transitions. For generating the counterexam- which sub-formula is more responsible for the
ple, DiPro Explored 480 traces in about 5 minutes satisfaction of ϕ along the paths.
resulting in 1685 vertices and 3291 edges. Finally,
the counterexample rendered consists just of 33 The results as generated by AMOS tool shows
diagnostic paths. It is evident that the number of ex- that C4 has the highest effect where C2 has more
plored vertices and explored edges while searching effect than C1 and C4 has more effect than C3.
the counterexample is always less than the number Performing a fast check on the dataset generated,
of states and the transitions of the model. It is also these explanations are confirmed, which means that
evident that the number of diagnostic paths is less along all the paths, C2 and C4 are usually the actual
than the number of solution traces. While solution causes not C1 and C3, with great notable presence
traces refer to all the paths of the diagnostic sub- for C4 comparing to C2.
graph found through exploring the model, diagnostic
Taking just M IP CX(s0 |= φ) to be the causality
paths refer just to the paths forming the counterex-
model instead of the whole model is due first to the
ample.
nature of M IP CX(s0 |= φ) itself; M IP CX(s0 |= φ)
We pass this counterexample to our algorithm for by definition covers the most probable causes for
generating the dataset of causes. The causes will the error, since it is consisting of paths with high
be the basic sub-formulas causing the satisfaction probabilities. Second, lowest probability values will
of ¬(down)U f ail io . For the right sub-formula, have no effect on the regression model generated
the cause generated is C0 = (count = since they tend to be zero. We tested this issue, by
M AX COU N T + 1). For the left sub-formula, the generating a counterexample for the property P =
set of causes is ?[¬(down)U f ail io].
C1 = ¬(i = 2), C2 = ¬(s < M IN SEN SORS) That is, the counterexample will consist of all paths
C3 = ¬(o = 2), C4 = ¬(a < M IN ACT U AT ORS) satisfying ¬(down)U f ail io, not just the paths with
C5 = ¬(count = M AX COU N T + 1) high probabilities. The counterexample generated
C6 = ¬(m = 0) consists of 132 paths, DipRo takes more than 30
minutes for computing this counterexample. Adding
After generating these causes with their probabilities the new paths (99 paths) to the old data set and
with respect to each path as a dataset, we found analysing it using AMOS did not bring considerable
the following results: along all paths (data rows), change to the previous regression model generated
C0 has the same probability. C2, C5 and C6 have depicted in Fig.3.
exactly equivalent probabilities with respect to each
path (data row). This means that they always occur 4.2. Polling Server System
together. As a result, before passing the data set
The system is modelled in PRISM as a CTMC, where
to AMOS tool, C0 will be ignored since its value
the number of stations handled by the polling server
is constant along all paths.C2, C5 and C6 will be
is denoted by N. Each station has a single-message
regrouped into one variable named (C2), since they
buffer and is cyclically attended by the server. We
share the same values. Thus, the final data set
choose the property that measures the probability of
will consist of the causes C1, C2, C3, C4 and the
station 1 being served (s=1) before station 2 (s=2)
‘until‘ formula ϕ denoted UF. For estimating the
where (a=1) denotes serving. This property is given
causal effect of each cause on UF, we generate
as follows:
the regression model based on this data set using
AMOS. The results as rendered by AMOS tool are
P =?[!(s = 2 ∧ a = 1)U (s = 1 ∧ a = 1)]
presented in Fig.3.
42
We test this property using PRISM for (N=3, N=5, 5. RELATED WORKS
N=7 and N=9). For all of these values, PRISM
renders a probability higher than 0.5. As a result, we Various approaches for probabilistic counterexam-
chose the value 0.5 as a threshold. The property can ple generation have been proposed. The authors
be rewritten as follows: (Aljazzar et al (2005), Aljazzar and Leue (2006)
introduced an approach for counterexample gener-
P ≤ 0.5[(!(s = 2)∨!(a = 1))U (s = 1 ∧ a = 1)] ation for DTMC and CTMC against timed reacha-
bility properties using heuristics guided and directed
We use DiPro to generate the counterexample, explicit state space search. In complementary work
which in turn uses PRISM. We have to specify the (Aljazzar and Leue (2009)), with the intuition that
model and the property to be verified, and then single scheduler makes an MDP as DTMC, they
DiPro computes the counterexample for violating the proposed an approach for counterexample gener-
probability threshold. We used the heuristic search ation for MDPs using existing methods for DTMC.
algorithm XBF that computes the counterexample They introduced more complete work in (Aljazzar
as a diagnostic sub-graph. Our method takes the and Leue (2010)) for generating counterexample as
counterexample generated from DiPro and the what they refer to as diagnostic sub-graphs. Based
property to be verified as parameters, and outputs on all the previous works, they built a tool, DiPro
the dataset. (Aljazzar and Leue (2011)), for generating coun-
terexamples for DTMC, CTMC and MDPs. Similar
The PRISM model consists of 1344 states and to the previous works, (Han et al. (2009)) has pro-
5824 transitions. For generating the counterexample, posed the notion of smallest most indicative coun-
DiPro Explored 184 traces in about 5 minutes terexample that reduces to the problem of finding
resulting in 1094 vertices and 3310 edges. Finally, K shortest paths. Instead of generating path-based
the counterexample rendered consists just of 18 counterexamples, the authors in (Wimmer et al.
diagnostic paths. It is evident that the number (2012)) have proposed a novel approach based on
of explored vertices and explored edges while critical subsystems. Following this work, the authors
searching the counterexample is always less than in (Jansen et al. (2012)) proposed the COMICS tool
the number of states and the transitions of the model. for generating the critical subsystems that induce
the counterexamples. Instead of relying on the state
We pass this counterexample to our algorithm for space search resulted from the parallel composition
generating the dataset of causes. The causes will of the modules, (Wimmer et al. (2013)) suggests
be the basic sub-formulas causing the satisfaction to rely directly on the guarded command language
of (!(s = 2)∨!(a = 1))U (s = 1 ∧ a = 1) . For the used by the model checker, which is more likely and
right sub-formula, the cause generated is C0 = (s = helpful for debugging purpose.
1 ∧ a = 1). For the left sub-formula, the set of causes
is C1 =!(a = 1) and C2 =!(s = 2). In conventional model checking, many works have
proposed techniques and algorithms for discovering
After generating these causes with their contribution error causes from counterexamples, hence present-
with respect to each path as a dataset, we found that ing them to the user in a comprehensive way. Most
C0 has the same probability along all paths (data of these works (Ball et al. (2003), Zeller et al. (2002),
rows). thus before passing the data set to AMOS Groce et al. (2003), Groce et al. (2006)) consider
tool, C0 will be ignored since its value is constant the existence of successful runs or executions to be
along all paths. The effect of C1 and C2 on U F compared with the error trace, with the assumption
is as generated by AMOS is given by the following that the more successful execution closed to the
equation: error trace indicates the causes of the error. Based
on Lewis counterfactual theory of causality (Lewis
(1973)) and distance metrics, the authors in (Groce
U F = −(0.304)C1 + (0.464)C2 (3) et al. (2006)) have proposed semi-automated ap-
proach for isolating errors in ANSI C programs by
The results as rendered by AMOS shows that C2 considering the alternative worlds as programs exe-
has higher effect than C1, where the effect of C1 cutions and the events as propositions about those
is negative. This means that the effect of C1 on executions. Unlike the previous works that require
U F increases once the paths probabilities get lower, multiple executions, the work (Wang et al. (2006))
which means that the presence of C1 increases just introduced a technique performed on a single con-
with in the paths with low probabilities. crete execution path using a weakest pre condition
algorithm. While all of these works addressed safety
properties, some of works attended to explain errors
43
for liveness properties that involve more computa- REFERENCES
tional complexity (Kumazawa and Tamai (2011)).
Aljazzar, H., Hermanns, H., Leue, S.(2005) Coun-
In recent work, (Debbi and Bourahla (2013))used terexamples for timed probabilistic reachability,
the definition of causality and its quantitative In: FORMATS 05. LNCS vol. 3829, pp. 177-195.
measure responsibility for analysing probabilistic Springer.
counterexamples of DTMCs and CTMCs. The
causes are given as pairs (state, variable) and Aljazzar, H., Leue, S.(2006) Extended directed
ordered with respect to such weights. Another search for probabilistic timed reachability. in
closely related to our work that of (Beer et al. (2011), FORMATS 06, LNCS vol. 4202, pp. 33-51.
Chockler et al. (2007)). They used the definition Aljazzar, H. and Leue, S.(2009) Generation of coun-
of causality for explaining LTL counterexamples in terexamples for model checking of markov deci-
(Beer et al. (2011)). Unlike addressing the question sion processes, In: Proc. of International Confer-
in (Beer et al. (2011)), what causes a system to ence on Quantitative Evaluation of Systems, pp.
falsify a specification? In the context of coverage 197-206.
(Chockler et al. (2007)), the question addressed
was: what causes a system to satisfy specification? Aljazzar, H. and Leue, S (2010) Directed explicit
In this aim, they adapt the definition of causality and state-space search in the generation of counterex-
its quantitative measure, responsibility (Chockler and amples for stochastic model checking. IEEE Trans.
Halpern (2004)). The definition of causality has also on Software Engineering vol. 36 , no. 1, pp. 37-60.
been used by (Kuntz et al. (2011); Leitner-Fischer
and Leue (2013) ). They adapted the definition Aljazzar, H. and Leue, S. (2011) DiPro - A Tool f or
of causality to event orders for generating fault Probabilistic Counterexample Generation, LNCS
trees from probabilistic counterexamples. In (Leitner- 6823, pp. 183-187. Aviable at http://www.inf.
Fischer and Leue (2013)) they proposed the notion uni-konstanz.de/soft/dipro/
of causality checking by integrating the causality Aziz, A., Sanwal, K., Singhal, V., Brayton R.(2000)
computation in the model checking algorithm itself Model-checking continuous-time Markov chains.
. ACM Trans on Computational Logic. vol. 1, no. 1,
pp. 162-170.
6. CONCLUSION AND FUTURE WORKS Baier, C., Haverkort, B., Hermanns, H., Ka-
toen J.-P.(2003) Model checking algorithms for
In this paper, we have shown how the notion of
continuous-time Markov chains. IEEE Trans on
causality can be interpreted in the context of prob-
Software Engineering, vol. 29, no. 7.
abilistic counterexamples. Due to the quantitative
nature of the causal model, we had to define for each Ball, T., Naik, M., Rajamani, S.K.(2003) From symp-
cause its contribution to the error. Following that, we tom to cause: localizing errors in counterexample
generate the regression model corresponding to the traces, In: POPL 2003, pp. 97-105.
causality model. For doing so, we have proposed
an algorithm for generating the causes as a data Beer, I., BenDavid, S., et al. (2011) Explaining
set. We have seen that delivering the causes for counterexamples using causality. Formal Methods
the violation of PCTL formula as a regression model Systems Design vol. 40, pp. 20–40.
stands as a good technique for describing the effect
Chockler, H., Halpern, J.(2004) Responsibility and
of variables with their values on the error.
blame: a structural-model approach, Journal of
Evidently, our approach does not ignore the previous Artificial Intelligence Research (JAIR) vol. 22, pp.
works of counterexample generation. But instead, it 93-115.
acts as a complementary task. Chockler, H., Halpern, J. Y., Kupferman, O.(2007)
What causes a system to satisfy a specification?.
As future works, We aim to show how our method
ACM Trans. on Computational Logic Vol.5, no. 5,
can perform on counterexamples generated from
pp. 1-24.
MDPs models. Furthermore, we plan to investigate
the problem of incomplete data, which is well known Debbi, H. and Bourahla, M.(2013) Causal Analysis
problem in regression, as well as the problem of of Probabilistic Counterexamples, in Proceedings
linear dependence between variables in the context of Eleventh ACM-IEEE International Conference
of probabilistic counterexamples. on Formal Methods and Models for Codesign
(MEMOCODE),pp . 77–86.
44
Debbi, H. and Bourahla, M.(2013) Generating Leitner-Fischer, F. and Leue, S.: Causality Checking
diagnoses for probabilistic model checking using for Complex System Models, in Proceedings of
causality, Journal of Computing and Information VMCAI ,LNCS, vol 7737, 2013, pp 248–276.
Technology vol. 21, no 1 pp . 13–23.
Eiter, T., Lukasiewicz, T.(2002) Complexity results Leitner-Fischer, F. and Leue, S.: Probabilistic fault
for structure-based causality. Artificial Intelligence, tree synthesis using causality computation.
vol. 142, pp. 53-89, Elsevier. International Journal of Critical Computer-Based
Systems, vol 4, no 2, 2013, pp 119–143.
Groce, A., Visser, W.: What went wrong(2003)
explaining counterexamples. In: Ball, T., Rajamani,
S.K. (eds.) SPIN, LNCS, vol. 2648, pp. 121-135. Lewis, D.: Causation (1973). Journal of Philosophy.
Vol. 70, pp. 556-567.
Groce, A., Chaki, S., Kroening, D., Strichman,
O.(2006) Error explanation with distance metrics. Muppala, J., Ciardo, G., and Trivedi, K. (1994)
STTT vol.8, no 3, pp. 229-247. Stochastic reward nets for reliability prediction,
Communications in Reliability, Maintainability and
Halpern, J., Pearl, J.: Causes and explanations Serviceability,vol.1, no.5.
(2001) A structural-model approach part I:
Causes. In: Proc. of 17th UAI, pp. 194–202. Wang, C., Yang, Z., Ivancic, F., Gupta A.(2006)
Morgan Kaufman Publishers. Whodunit? Causal Analysis for Counterexam-
ples. In:Proc.of the International Symposium
Han, T., Katoen, J.P.(2009) Counterexamples Gener- on Automated Technology for Verification and
ation in probabilistic model checking. IEEE Trans- Analysis (ATVA).
actions on Software Engineering 35(2).pp. 72–86.
Wimmer, R., Jansen N., Abraham E., Becker B.,
Hansson, H., Jonsson B.(1994) logic for reasoning Katoen J.P (2012) Minimal Critical Subsystems for
about time and reliability. Formal aspects of Discrete-Time Markov Models, in TACAS, LNCS
Computing, vol. 6, no. 5, pp. 512-535. vol.7214 , pp . 299-314.
Hinton A., Kwiatkowska M., Norman G., Parker D.: Wimmer, R., Jansen N., Vorpahl A. (2012) High-
PRISM (2006) A tool for automatic verifi-cation of Level Counterexamples for Probabilistic Automata,
probabilistic systems. In Proc. 12th International in Quantitative Evaluation of Systems (QEST),
Conference on Tool s and Algo-rithms for the LNCS vol.8054 , 2013, pp . 39-54.
Construction and Analysis of Systems (TACAS
06). LNCS, vol. 3920, pp. 441-444. Wright, Sewall S.: Correlation and causation. Journal
of Agricultural Research, vol. 20, 1921, pp. 557-
Ib, O. C. and Trivedi, K.(1990) Stochastic petri 585.
net models of polling systems, IEEE Journal on
Selected Areas in Communications, vol. 8 , no. 9, Zeller, A.(2002) Isolating cause-effect chains from
pp.1649-1657. computer programs. In: SIGSOFT 2002/FSE 10,
pp. 1-10.
Jansen N., Abraham E., Volk, M., Wilmer, R., Katoen
J.P and Becker B. (2012) The COMICS Tool - AMOS, http://amosdevelopment.com/download/.
Computing Minimal Counterexamples for DTMCs,
in ATVA, LNCS vol.7561, pp. 249-353. Cyclic Server Polling System: available at
Katoen J.-P., Khattri M., Zapreev I. S.(2005) http://www.prismmodelchecker.org/casestudies/polling.php.
A Markov Reward Model Checker. in Second /embedded.php.
International Conference on the Quantitative
Evaluation of systems (QEST 2005). pp.243-244. Embedded Control System: available at
IEEE Computer Society. http://www.prismmodelchecker.org/casestudies/embedded.php
Kumazawa, T., Tamai, T.2011) Counterexample-
Based Error Localization of Behavior Models.
NASA Formal Methods, pp. 222–236.
Kuntz, M., Leitner-Fischer, F., Leue, S. (2011) From
probabilistic counterexamples via causality to fault
trees. LNCS, vol 6894, pp . 71-84.