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) has appeared
as an extension of model checking for modelling and
analysing systems that exhibit stochastic behaviour.
Several case studies in several domains have been
addressed from randomized distributed algorithms
and network protocols to biological systems and
cloud computing environments. These systems
are described usually using Discrete-Time Markov
Chains (DTMC), Continuous-Time Markov Chains
(CTMC) or Markov Decision Processes (MDP), and
verified against properties specified in Probabilistic
Computation Tree Logic (PCTL)
Generating small and indicative counterexamples
only is not enough for understanding the error.
Therefore, in conventional model checking, many
works have addressed the analysis of
counterexamples to understand the failure (
This paper contains two complementary
contributions. The first defines a formal causality model for
the counterexample, where we give the definition of
an actual cause for the violation of PCTL/CSL
formula = P p('). The second complements the first
by generating a regression model from the causality
model, which quantifies the effect of each cause on
the violation of the PCTL/CSL formula. In this paper,
we will focus on upper bounded properties. Lower
bounded properties can be transformed easily to
upper bounded properties (
The rest of this paper is organized as follows. In Section 2, we present some preliminaries and definitions. The Probabilistic Computation Tree Logic (PCTL) and probabilistic counterexamples are presented in this section. In section 3, we give the definition of Causes in probabilistic counterexamples with the formal causality model, and then we show how to generate the regression model from it. Following that, we introduce an algorithm for generating the causes of violation of PCTL/CSL properties and the related regression model. Section 4 describes an experimental study. Section 5 presents the related works. At the end, we present conclusion and future works.
A Discrete-Time Markov Chain (DTMC)is a tuple D = (S; sinit; P; L) , such that S is a finite set of states, sinit 2 S the initial state,P : S S ! [0; 1] represents the transition probability matrix, L : S ! 2AP is a labelling function that assigns to each state s 2 S the set L(s) of atomic propositions. An infinite path is a sequence of states s0s1s2::: , where 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 starting from a state s0 by P aths(s0). The underlying -algebra is formed by the cylinder sets which are induced by finite paths in P aths(s0). The probability of this cylinder set is:
P ( 2 P aths(s0)js0s1:::snis a prefix of ) =
Qi 0<n P (si; si+1) The Probabilistic Computation Tree Logic (PCTL) has appeared as an extension of CTL for the specification of systems that exhibit stochastic behaviour. We use the PCTL for defining quantitative properties of DTMCs. PCTL state formulas are formed according to the following grammar: ::= truejaj: j 1 ^ 2jP p(') Where a 2 AP is an atomic proposition, ' is a path formula, P is a probability threshold operator, 2 f<; ; >; g is a comparison operator, and p is a probability threshold. The path formulas ' are formed according to the following grammar: ' ::= 1U 2j 1W 2j 1U n 2j 1W n 2 Where 1and 2 are state formulas and n 2 N . As in CTL, the temporal operators (U for strong until, W for weak (unless) until and their bounded variants) are required to be immediately preceded by the operator P. The PCTL formula is a state formula, where path formulas only occur inside the operator P. The operator P can be seen as a quantification operator for both the operators 8 (universal quantification) and 9 (existential quantification), since the properties are representing quantitative requirements.
The semantics of a PCTL formula over a state s (or a path ) in a DTMC model D = (S; sinit; P; L) can be defined by a satisfaction relation denoted by j=. The satisfaction of P p(') on DTMC depends on the probability mass of set of paths satisfying '. This set is considered as a countable union of cylinder sets, so that, its measurability is ensured.
The semantics of PCTL state formulas for DTMC is defined as follows: s j= true , true s j= a , a 2 L(s) s j= : , s 6j= s j= 1 ^ 2 , s j= 1 ^ s j= s j= P p(') , P (s j= ') p 2 Given a path = s0s1::: in D and an integer j 0, where [j] = sj , The semantics of PCTL path formulas for DTMC is defined as for CTL as follows: j= 1U 2 , 9j j: [k] j= 1) j= j= j: [k] j= 1)
j= 1W n 2 , n: [k] j= 1) 11UW n2 , j= 2 , 90 0: [j] j= 2 ^ (80
k < 1U 2 _ (8k j n: [j] j= 0: [k] j= 2 ^ (80 1) k < j= 1U n 2 _ (80 k For specifying properties of CTMC, we use The Continuous Stochastic Logic (CSL). CSL has the same syntax and semantics as PCTL, except that in CSL, the time bound in bounded until formula can be presented of an interval of non-negative reals. Before verifying CSL properties over CTMC, the CTMC has to be transformed to its embedded DTMC. Therefore, further description of CTMC model checking is beyond the scope of this paper. We refer to [2, 3] for further details. In the rest of paper, we refer to probabilistic formula PCTL/CSL as = P p(').
The probabilistic counterexample is generated
when a PCTL/CSL property is not satisfied. The
probabilistic property = P p(') is refuted when
the probability mass of the paths satisfying '
exceeds the bound p. Therefore, a probabilistic
counterexample for the property is formed by
a set of paths starting at state s and satisfying
the path formula '. We denote these paths by
P aths(s0 j= ). The counterexample can be formed
of set of finite paths where each path = s0s1:::sn
is a prefix of an infinite path from P aths(s0 j= )
satisfying the formula '.We denote these paths by
F initeP aths(s0 j= ). These finite paths are also
called diagnostic paths (
It is clear that we can get a set of probabilistic counterexamples, noted P CX(s0 j= ), which is a set of any combination from F initeP aths(s0 j= ) that their probability mass exceeds the bound p. Among all these probabilistic counterexamples, we are interested by the most indicative one. The most indicative counterexample is minimal counterexample (has the least number of paths from F initeP aths(s0 j= )) and its probability mass is the highest among all other minimal counterexamples. We denote the most indicative probabilistic counterexample by M IP CX(s0 j= ). We should note that the most indicative probabilistic counterexample may not be unique.
For the counterexample to have high probability, it should consist of paths that carry high probabilities from F initeP aths(s0 j= ). The path having the highest probability over all these paths is called strongest path and is defined as follows: for every path 0 2 F initeP aths(s0 j= ) : P ( ) P ( 0). The strongest path also may not be unique.
Lemma 2.1 A most indicative probabilistic counterexample M IP CX(s0 j= ) contains at least one strongest path 2 F initeP aths(s0 j= ).
Lemma 2.2 For every path on which the property 1U 2 2 M IP CX(s0 j= ) ( 1U n 2) is satisfied, the right state sub-formula ( 2) is satisfied in the last state of .
Example 1 Let us consider the example of DTMC shown in Figure 1 and the property P 0:7('), where ' = (a _ b)U (c ^ d). The property above is violated in this model (s0j 6j= P 0:7(')), since there exists a set of paths satisfying ' whose probability mass is higher than the probability bound (0.7). Any combination from F initeP aths(s0 j= ) having probability mass higher than 0.7, is a valid counterexample including the whole set. For instance, we can find three counterexamples: F initeP aths(s0 j= ) = fs0s2s3; s0s1s4; s0s2s4; s0s1s3; s0s2s1s4; s0s1s2s3; s0s2s1s3; s0s1s2s4g Any combination of finite paths from F initeP aths(s0 j= ) having probability mass higher than 0.7, is a valid probabilistic counterexample including the whole set. We can find three counterexamples: P (CX1) = P (fs0s2s3; s0s1s4; s0s2s4; s0s1s3; s0s2s1s4; s0s1s2s3; s0s2s1s3; s0s1s2s4g) = 0:24 + 0:16 + 0:12 + 0:09 + 0:072 + 0:064 + 0:036 + 0:032 = 0:804 The last probabilistic counterexample is the most indicative since it is minimal and its probability is higher than the other minimal counterexample CX2,P (CX3) > P (CX2).The strongest path is P (s0s2s3) = 0:24, which is included in the most indicative probabilistic counterexample.
Halpern and Pearl (
We call a Boolean combination of primitive events a basic causal formula. We call a Boolean combination of basic causal formulas a causal formula. A causal formula ' is true or false in causal model, given a context. We write (M; !u ) j= ' if ' is true in causality model M given a context !u , where !u represents a setting for the variables in U. We write (M; !u ) j= [!Y !y](X = x), where !Y V , if X has a value x in M given a context !u and the assignment !y to !Y. The formulas that are allowed to be causes for ' are ones of the form X1 = x1 ^ ::: ^ Xk = xk which is abbreviated to the form !X = !x . With all these definitions in hand, we can now give the definition of an actual cause by Halpern and Pearl.
Definition 2.1 (Actual Cause) we say that !X = !x is an actual cause of ' in (M; !u ) if the following holds: 1. (M; !u ) j= (!X = !x ) ^ ' 2. There exists a partition ( !Z; W!) of V with !X !Z and some setting (!x 0; !w0) of the variables in (!X; W!) such that if (M; !u ) j= Z = z for Z 2 !Z, then a-(M; !u ) j= h!X !x 0; W! !w0i ^ :' b(M; !u ) j= h!X for all subsets !Z0 of !Z.
!x ; W!
!i !w0; !Z0 z ^ ' 3. The set of variables !X is minimal (no subset of !X satisfies the conditions 1 and 2).
The first condition states that both !X = !x and ' are
true in the current context, given the variables !X and
their values !x . The second condition states that any
change on (!X; W!) will change ' from true to false,
changing W! will have no effect on ' as long as the
values of !X are kept at the current values, even if
all subsets !Z0 of !Z are set to their original values
in the current context. Minimality condition ensures
that only elements in the conjunction !X = !x are
essential for changing ' from true to false. As a
consequence of this condition, we can refer to a
cause as X = x, because the causes can always be
taken to be single conjuncts (
Regression analysis is a statistical technique enables us to reason about the relationship between variables. It describes the change in value of a variable Y , namely dependent or endogenous in response to the variation of a variable X namely independent or exogenous. The relationship between these variables is either positive or negative. If the value of Y increases when the value of X rises, it is said that the relationship is positive. Conversely, the relationship is said to be negative. One of the relationships that we can infer and statistically reason about using regression analysis is causality. The causal model is build based on assumptions or hypothesis, and then is tested against statistical data to determine how the specified model fits the data. So when it comes to causal relationships, we can use regression analysis to estimate the causal effect instead of exploring the causal relationships. The causal relationship between dependent variable Y and independent variable X with the consideration of factors noise called disturbance term or error term and denoted " is given by the linear equation
Y = X + " (1) Where X stands as a cause for Y , stands as a coefficient or weight that quantifies the direct causal effect of X on Y . " is an error term stands for all extraneous variables, which are assumed to be uncorrelated with X. Whereas the variables X and Y are perfectly known, the objective behind using regression analysis is to produce an estimate of the two parameters and ".
For probabilistic properties of the form = P6p(') , explaining the violation reduces to the explanation of exceeding the probability bound over the DTMC model. Therefore, the question:what labelling and/or probability values in the counterexample causes the system to falsify a specification, reduces to the question: what labelling and/or probability values in the counterexample causes the exceeding of probability bound over the model.
A causality model for the most indicative probabilistic counterexample M IP CX(s0 j= ) is a tuple M = (U; V; F ), where the set U is represented by a context variable; its value u represents a state s 2M IP CX(s0 j= ). V is a set of atomic propositions and Boolean formulas. F associates with every variable Vi 2 V a truth function fVi that determines the value of Vi (0 or 1), given a state s and the values of other variables in V .
For example, fp^r(s; p = 1; r = 1) = 1 where p and r are atomic propositions, and s is state representing a context. The causal influence is modelled by the transitions in M IP CX(s0 j= ).
Let us denote by M IP CX(s\;Xx0)(s0 j= ) the set of finite paths resulted from M IP CX(s0 j= ) by switching the value of a variable X 2 V in a state s.
counterexample M IP CX(s0 j= ) for a probabilistic formula = P p('), a state s 2 M IP CX(s0 j= ) and a variable X 2 V has a value x 2 f0; 1g in s. We say that (X = x) is critical for the violation of = P p(') in s, if M IP CX(s\;Xx0)(s0 j= ) is not a valid counterexample for = P p(').
That is, for the probabilistic counterexample M IP CX(s0 j= ), we say that the value of a variable X is critical for the violation of = P p(') in a state s, if changing the value of X in this state renders the result not a counterexample.
Definition 3.3. (Actual Cause) Consider a counterexample M IP CX(s0 j= ) for a probabilistic formula = P p(') and a variable X 2 V . We say that (X = x) is a cause for the violation of = P p(') in s, if (X = x) is critical , or there exists a subset of variables W!of V in s such that switching the values !w of W in s makes (X = x) critical. Thus, in our setting, we can refer to a cause as (X = x) where X is an atomic proposition has the value 1 in s if X 2 L(s), and it has the value 0 otherwise. (X = x) is said to be cause in state s, if it is critical, or it can be made critical by switching the values of set of variables W in s.
Definition 3.4. A Diagnostic causality model for M IP CX(s0 j= ) is a tuple hM; CC i, where M is a causality model, and CC is a contribution function that assigns to each cause its contribution to the satisfaction of ' with respect to a path 2 M IP CX(s0 j= ) as follows
(2)
X s2 jfX (s)=x That is, with respect to each path 2 M IP CX(s0 j= ), we have associated to each cause a measure that represents the sum of probabilities of reaching the states in which X = x. We can say that X = x is a cause for the satisfaction of ' with respect to a path with a contribution CC . So, the cause having the highest contribution will be the one found the most along the path.
Example. Consider the most indicative counterexample
CX3 = fs0s2s3; s0s1s4; s0s2s4; s0s1s3; s0s2s1s4; s0s1s2s3g generated from the DTMC presented in Fig1 against the property P 0:7('), where ' = (a _ b)U (c ^ d). It is possible to define a causality model for CX3, where u 2 fs0; s1; s2; s3; s4; s5g, and F can be defined over the variables in V as follows
fa(s1) = 1 fc^d(s1; c = 0; d = 0) = 0
...
For instance, it is clear that in s2, the actual cause for the satisfaction of ' = (a _ b)U (c ^ d) is b = 1. The probability of the actual cause b = 1 in the path 2 = s0s2s3 is CC 2 (b = 1) = 0:6.
We aim now quantify the effect of a cause X = x on the violation of . To do so, we use the regression analysis as a comprehensive technique for estimating this effect, where the path formula ' will stand as a dependent variable, whereas the formula of the form X = x will stand as an independent variable. So, the regression model will describe the behaviour of the system by analysing the change of the probability of ' satisfaction with respect to variables that are considered to be causes.
While the variables are now well defined, the remaining task is to generate the data required for estimating the structural parameters. With respect to the definition of diagnostic causality model, we have seen that each cause X = x has a contribution CC (X = x) with respect to each path 2 M IP CX(s0 j= ). So in our setting, P ( ) will stand for the value of ' and CC (X = x) will stand for the value of X = x . As a result, the number of data rows will be exactly the number of finite paths forming the M IP CX(s0 j= ). We present an algorithm for generating the causes and their contributions, hence constructing the data set.
This algorithm performs on counterexample
generated by the tool DiPro (
Inputs: The probabilistic formula = P p(')
The counterexample M IP CX(s0 j= ) Outputs: DataSet: Variables (causes) with values (CC ) begin
Causes := ? for each path 2 M IP CX(s0 j= ) do for each state s 2 do if s is the last state in then
Causes := findCauses(s; 2)
CC (Causes) = Ps2 jfX (s)=x P (s) end if else
Causes := findCauses(s; 1)
CC (Causes) = Ps2 jfX (s)=x P (s) end else end for end for end ComputeDataset function findCauses(s, ) begin if is of the form 1 ^ 2 then return findCauses(s, 1) [ findCauses(s, 2) end if If is of the form 1 _ 2 Then
If s j= 1 and s j= 2 Then
return FindCauses(s, 1) [ FindCauses(s, 2) End If If s j= 1 and s 6j= 2
return FindCauses(s, 1) End If If s 6j= 1 and s j= 2
return FindCauses(s, 2)
End If End If if is of the form a where a 2 AP and a 2 L(s) then return a end if if is of the form :a where a 2 AP and a 2= L(s) then return:a end if end findCauses The algorithm explores the counterexample path by path, and computes the causes that will act as data variables, and computes their probabilities that will act as data values. We notice that these two tasks are performed simultaneously. We compute CC (X = x) of each cause X = x found in set of states. The condition put on last state follows Lemma 2.3. The main function of this algorithm is FindCauses. It takes a state and state formula as input and returns recursively a set of causes. We note that when the state formula is of the form 1 ^ 2, both sub-formulas are essentially true at state s. But When is of the form 1 _ 2, one of them could be true at s or both of them. This actually follows the causal intuition that in conjunctive scenario, both 1and 2 are required for being satisfied, whereas in the disjunctive scenario, either 1 or 2 suffices to make satisfied. In the two cases, we apply FindCauses to each sub-formula. Finally, at the propositional level, the cause would be a(a = 1) or :a(a = 0), and it is allowed to be a conjunction of primitive formulas.
The Algorithm over-approximates the set of causes
, since computing the set of causes exactly in
binary causal models is NP-complete (
It is evident that the complexity of this algorithm is
polynomial in size of M IP CX(s0 j= ) and the size
of '. This follows from the fact that the left
subformula 1 is evaluated in each state except the last
ones, in which the right sub-formula 2 is evaluated,
this is much less hard than evaluating both
subformulas at each state of the counterexample (
We modelled the DTMC presented before in Fig.1 in PRISM. Then we generate most indicative counterexample using DiPro for the property P 0:7('). The counterexample generated is CX3 where We pass the counterexample to be analyzed to our algorithm, which is implemented in Java. It takes the counterexample generated by DiPro in XML 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 = fc; dg These causes denoted Ci stand as independent variables (X) for the regression model we are going to build, where the until formula ' denoted UF stands for the dependent variable (Y). The data values of these observed variables are given in the table bellow
UF 0.24 0.16 0.12 0.08 0.072 0.064
C1 1 1.04 1 1.04 1.03 1.04
C2 As we see in the table, the number of data rows represents the number of paths of M IP CX(s0 j= ), where the value of until formula UF refers to the probability of each path P ( ) and the value of cause refers to CC (X = x) .
We have implemented the above method in Java.
To evaluate our method, we use two benchmark
case studies, the embedded control systems taken
from (
The system consists of input processor (I) that reads incoming data from three sensors (s1,s2,s3) and then passes it to main processor (M). The processor M processes the data and sends instructions to an output processor (O) that controls two actuators (A1 and A2) using these instructions.Any of the system’s components M, I/O, the sensors and the actuators may fail; as a result the system is shut down. The types of failure are: f ail sensors = (i = 2 ^ s < M IN SEN SORS) f ail actuators = (o = 2^a < M IN ACT U AT ORS) f ail io = (count = M AX COU N T + 1) f ail main = (m = 0) We use the variable M ax Count to refer to the maximum number of consecutive cycles skipped allowed. Thus, the I/O processor will fail if the count exceeds the limit M ax Count. The down status of the system is labelled as:
down = f ail sensorsjf ail actuatorsjf ail iojf ail main That is, the systems is down if any of this failures occurs. For this model, we choose the property that estimates the probability of I/O failure occurring first, which is given as follows:
P =?[:(down)U f ail io] We test this property using PRISM for (M ax Count = 6). For this value, PRISM renders a probability equal to 0.11. We chose the value 0.1 as a threshold for this property to generate the counterexample. Thus the property can be rewritten as follows:
P
0:1[:(down)U f ail io] We use DiPro to generate the counterexample, which in turn uses PRISM. The counterexample can be rendered graphically and stored in XML format. The tool implements many algorithms. In our experiments, we used the heuristic search algorithm XBF that computes the counterexample as a diagnostic sub-graph. Our method takes the counterexample generated from DiPro in XML format and the property to be verified , and outputs the causes and their values as a dataset in Excel file. This excel file is passed to the tool AMOS in order to generate the regression model. AMOS is wellknown software for SEM that enables user to specify, confirm and refine models, by incorporating many statistical methods. The PRISM model consists of 6858 states and 28907 transitions. For generating the counterexample, DiPro Explored 480 traces in about 5 minutes resulting in 1685 vertices and 3291 edges. Finally, the counterexample rendered consists just of 33 diagnostic paths. It is evident that the number of explored vertices and explored edges while searching the counterexample is always less than the number of states and the transitions of the model. It is also evident that the number of diagnostic paths is less than the number of solution traces. While solution traces refer to all the paths of the diagnostic subgraph found through exploring the model, diagnostic paths refer just to the paths forming the counterexample.
We pass this counterexample to our algorithm for generating the dataset of causes. The causes will be the basic sub-formulas causing the satisfaction of :(down)U f ail io . For the right sub-formula, the cause generated is C0 = (count = M AX COU N T + 1). For the left sub-formula, the set of causes is C1 = :(i = 2), C2 = :(s < M IN SEN SORS) C3 = :(o = 2), C4 = :(a < M IN ACT U AT ORS) C5 = :(count = M AX COU N T + 1) C6 = :(m = 0) After generating these causes with their probabilities with respect to each path as a dataset, we found the following results: along all paths (data rows), C0 has the same probability. C2, C5 and C6 have exactly equivalent probabilities with respect to each path (data row). This means that they always occur together. As a result, before passing the data set to AMOS tool, C0 will be ignored since its value is constant along all paths.C2, C5 and C6 will be regrouped into one variable named (C2), since they share the same values. Thus, the final data set will consist of the causes C1, C2, C3, C4 and the ‘until‘ formula ' denoted UF. For estimating the causal effect of each cause on UF, we generate the regression model based on this data set using AMOS. The results as rendered by AMOS tool are presented in Fig.3. 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 are facing a disjunctive scenario for both failures. In fact, the weights presented above have more importance when we face a disjunctive scenario ( 1 _ 2), because the designer will need to know which sub-formula is more responsible for the satisfaction of ' along the paths.
The results as generated by AMOS tool shows that C4 has the highest effect where C2 has more effect than C1 and C4 has more effect than C3. Performing a fast check on the dataset generated, these explanations are confirmed, which means that along all the paths, C2 and C4 are usually the actual causes not C1 and C3, with great notable presence for C4 comparing to C2.
Taking just M IP CX(s0 j= ) to be the causality model instead of the whole model is due first to the nature of M IP CX(s0 j= ) itself; M IP CX(s0 j= ) by definition covers the most probable causes for the error, since it is consisting of paths with high probabilities. Second, lowest probability values will have no effect on the regression model generated since they tend to be zero. We tested this issue, by generating a counterexample for the property P = ?[:(down)U f ail io].
That is, the counterexample will consist of all paths satisfying :(down)U f ail io, not just the paths with high probabilities. The counterexample generated consists of 132 paths, DipRo takes more than 30 minutes for computing this counterexample. Adding the new paths (99 paths) to the old data set and analysing it using AMOS did not bring considerable change to the previous regression model generated depicted in Fig.3.
The system is modelled in PRISM as a CTMC, where the number of stations handled by the polling server is denoted by N. Each station has a single-message buffer and is cyclically attended by the server. We choose the property that measures the probability of station 1 being served (s=1) before station 2 (s=2) where (a=1) denotes serving. This property is given as follows:
P =?[!(s = 2 ^ a = 1)U (s = 1 ^ a = 1)] We test this property using PRISM for (N=3, N=5, N=7 and N=9). For all of these values, PRISM renders a probability higher than 0.5. As a result, we chose the value 0.5 as a threshold. The property can be rewritten as follows:
P
0:5[(!(s = 2)_!(a = 1))U (s = 1 ^ a = 1)] We use DiPro to generate the counterexample, which in turn uses PRISM. We have to specify the model and the property to be verified, and then DiPro computes the counterexample for violating the probability threshold. We used the heuristic search algorithm XBF that computes the counterexample as a diagnostic sub-graph. Our method takes the counterexample generated from DiPro and the property to be verified as parameters, and outputs the dataset.
The PRISM model consists of 1344 states and 5824 transitions. For generating the counterexample, DiPro Explored 184 traces in about 5 minutes resulting in 1094 vertices and 3310 edges. Finally, the counterexample rendered consists just of 18 diagnostic paths. It is evident that the number of explored vertices and explored edges while searching the counterexample is always less than the number of states and the transitions of the model. We pass this counterexample to our algorithm for generating the dataset of causes. The causes will be the basic sub-formulas causing the satisfaction of (!(s = 2)_!(a = 1))U (s = 1 ^ a = 1) . For the right sub-formula, the cause generated is C0 = (s = 1 ^ a = 1). For the left sub-formula, the set of causes is C1 =!(a = 1) and C2 =!(s = 2).
After generating these causes with their contribution with respect to each path as a dataset, we found that C0 has the same probability along all paths (data rows). thus before passing the data set to AMOS tool, C0 will be ignored since its value is constant along all paths. The effect of C1 and C2 on U F is as generated by AMOS is given by the following equation:
U F = (0:304)C1 + (0:464)C2 (3) The results as rendered by AMOS shows that C2 has higher effect than C1, where the effect of C1 is negative. This means that the effect of C1 on U F increases once the paths probabilities get lower, which means that the presence of C1 increases just with in the paths with low probabilities.
Various approaches for probabilistic
counterexample generation have been proposed. The authors
(
In conventional model checking, many works have
proposed techniques and algorithms for discovering
error causes from counterexamples, hence
presenting them to the user in a comprehensive way. Most
of these works (
In this paper, we have shown how the notion of causality can be interpreted in the context of probabilistic counterexamples. Due to the quantitative nature of the causal model, we had to define for each cause its contribution to the error. Following that, we generate the regression model corresponding to the causality model. For doing so, we have proposed an algorithm for generating the causes as a data set. We have seen that delivering the causes for the violation of PCTL formula as a regression model stands as a good technique for describing the effect of variables with their values on the error.
Evidently, our approach does not ignore the previous works of counterexample generation. But instead, it acts as a complementary task.
As future works, We aim to show how our method can perform on counterexamples generated from MDPs models. Furthermore, we plan to investigate the problem of incomplete data, which is well known problem in regression, as well as the problem of linear dependence between variables in the context of probabilistic counterexamples.