1

Automatically ‘Verifying’ Discrete-Time Complex
Systems through Learning, Abstraction and
Refinement
Jingyi Wang, Jun Sun, Shengchao Qin, and Cyrille Jegourel
Abstract—Precisely modeling complex systems like cyber-physical systems is challenging, which often render model-based systemverification techniques like model checking infeasible. To overcome this challenge, we propose a method called LAR to automatically‘verify’ such complex systems through a combination of learning, abstraction and refinement from a set of system log traces. We
assume that log traces and sampling frequency are adequate to capture ‘enough’ behaviour of the system. Given a safety property andthe concrete system log traces as input, LAR automatically learns and refines system models, and produces two kinds of outputs. One
is a counterexample with a bounded probability of being spurious. The other is a probabilistic model based on which the given property
is ‘verified’. The model can be viewed as a proof obligation, i.e., the property is verified if the model is correct. It can also be used for
subsequent system analysis activities like runtime monitoring or model-based testing. Our method has been implemented as aself-contained software toolkit. The evaluation on multiple benchmark systems as well as a real-world water treatment system shows
promising results.
Index Terms—Verification, model learning, abstraction refinement, Cyber-physical systemF

1

I NTRODUCTIONYBER - PHYSICAL systems (CPS) integrate physical and engineered systems and have the potential to transform the way
people interact with engineered systems. They are often used tocontrol public infrastructures like water purification/distribution
systems or smart grid systems. When CPS are employed insuch safety-critical scenarios, it is desirable to show that they
can operate dependably and safely. Analyzing CPS, however, ischallenging. Existing system analysis methods, like model-based
testing, model checking and theorem proving, require the availability of a system model. Because CPS closely interact with thephysical environment, the model must not only capture the systembehavior but also the environment’s. Modeling the environmentis often hard, due to complicated continuous dynamics in thephysical environment.
CPS are merely an example of those complex systems forwhich manual modeling is challenging. To tackle the challenge, multiple approaches that do not rely on manual modeling
have been explored. One example is statistical model checking(SMC) [58]. The idea is to provide a statistical measure on thelikelihood of satisfying a given property, by observing sample
system traces and applying techniques like hypothesis testing [28],

C

•
•
•
•
•

Jingyi Wang is with College of Computer Science and Software Engineering, Shenzhen University, China. He is also with Singapore University ofTechnology and Design, Singapore. E-mail: jingyi wang@sutd.edu.sg
Jun Sun, the corresponding author, is with Singapore University of Technology and Design, Singapore. E-mail: sunjun@sutd.edu.sg.
Shengchao Qin is with School of Computing, Media and the Arts, Teesside
University, UK. He is also with College of Computer Science and Software
Engineering, Shenzhen University, China. E-mail: S.Qin@tees.ac.uk
Cyrille Jegourel is with Singapore University of Technology and Design,
Singapore. E-mail: cyrille jegourel@sutd.edu.sg
This work was supported in part by National Natural Science Foundationof China under Grant No. 61772347 and Science and Technology Foundation of Shenzhen City under Grant No. JCYJ20170302153712968.

[58]. However, SMC has its limitations. For instance, since SMC
relies on sampling finite system traces, it is challenging to verify
un-bounded properties [46], [56], like eventually always something good happens. Furthermore, when SMC claims a property isverified, it provides no insight on why the property holds. If a newproperty is given, SMC must be applied from scratch. Anotherapproach for avoiding manual modeling is to automatically learn
models from system logs (i.e., sample system traces). Multiple
learning algorithms have been proposed to learn a variety ofmodels, e.g., [13], [21], [48], [49]. It has been shown that suchlearned models can be useful for system analysis in certain
scenarios. Recently, the idea has been extended to learn models
for system verification through model checking. In [16], [40],[41], [42], the authors proposed to learn probabilistic models andthen apply techniques like probabilistic model checking (PMC)
to calculate the probability of satisfying a property based on thelearned model. Compared to SMC, learning could be beneficial as
it overcomes several known limitations with SMC. For instance,
we can verify unbounded properties based on the learned model.
Furthermore, the learned model could be useful for a range ofsystem analysis or control objectives, e.g., for model-based testing
and for implementing runtime monitors.
Existing learning methods [13], [16], [21], [40], [41], [48],[49] however have multiple issues. Firstly, they are designed witha fixed level of abstraction, which limits their applicability to realworld systems. For instance, the traces we obtain from a realworld water treatment system [3] capture the reading of 25 sensors
plus 26 variables used in the control software. Furthermore, thesevariables are mostly float or double. Without abstraction, it ishard to learn a precise and reasonably small model of the system.
Determining the right level of abstraction is however highly nontrivial. As far as we know, it has not been investigated on how
to learn probabilistic models at the right level of abstraction.
Secondly, existing learning methods do not take into account the2property to be verified. In a recent empirical study [55], it isobserved that the verification results based on the learned models
could deviate significantly from the actual results.
In this work, we aim to develop a method to ‘verify’ CPS
by learning models at a level of abstraction which is ideal forverifying or falsifying the given property, and by generating
verification results which are validated against the actual system. The method we propose is called LAR, which is a novel
combination of probabilistic model learning and counterexample
guided abstraction refinement (CEGAR) [17], [18], [31]. Combing
learning and CEGAR is far from straightforward, due to the lackof a “ground-truth” model.
The overall workflow is shown in Fig. 1. The input of LAR
includes a probabilistic property and a set of system traces, which
could be obtained from a logger in the system. We assume
that the logging mechanism (i.e., the logged variables and thelogging frequency) are adequate to capture ‘enough’ behaviourof the system regarding the property. We first construct a set of
abstract system traces through predicate abstraction. Next, weapply existing automatic model learning techniques to constructa probabilistic model of the system, in the form of a discrete
time Markov chain (DTMC). Afterwards, we apply PMC to verify
the model against the property. If a counterexample is identified,
we check whether the counterexample, in the form of a set ofpaths of the learned model, is spurious. Notice that because we
do not have a model of the system, we cannot completely verify
whether the counterexample is spurious or not. We solve theproblem by applying hypothesis testing to bound the probabilityof the counterexample being spurious. If the counterexample is not
spurious, we report that the system fails the property. Otherwise,
we analyze the counterexample to generate a new predicate which
would rule out the counterexample.
Due to the lack of a system model, standard methods for generating new predicates (e.g., weakest pre-condition calculation [18]or interpolation [29]) are infeasible. We solve the problem byadopting classification techniques from the machine learning
community (refer to Section 3.4 for details). We then repeat theprocess until either we have identified a counterexample or haveconstructed a probabilistic model of the system based on which
the property is verified. In the latter case, the model generated
by our method could be viewed as a proof obligation (i.e., theproperty is verified if the model is correct), which could befurther evaluated by experts or through other means (like statistical
validation of the model). Furthermore, our learned models can bepotentially used for many subsequent system analysis activities.
For instance, we could use the models for model checking [38]and implementing runtime monitors [51]. The models can also
help design more robust systems [33]. We could also use themfor model-based testing to generate more useful test cases [44].
Lastly, our method has the potential to help people understandhow a complex system works by automatically extracting relevant
predicates. We implemented our method as a software toolkit andapplied it to benchmark systems and a real-world water treatment
system. The evaluation validated our approach well.
The remainder of the paper is organized as follows. Section 2
reviews necessary background and defines our problem. Section 3
presents the details of our approach. Section 4 presents our implementation and evaluates our method. Section 5 reviews related
work and Section 6 concludes.

2

BACKGROUND

System Assumptions. We assume that the system under analysis, denoted as M , has n observable variables, i.e., VM ={V1 , V2 , · · · , Vn }. Each variable Vi is associated with a domain
Di which may have infinite values. For instance, the variables ina water treatment system include those variables in the control
software (with finite domains) as well as those representing theenvironment (with infinite domains). We assume that M is acomplicated system such that we do not know exactly how thevariables VM change. However, we assume that M is deterministic if VM is fully observed, i.e., the same sequence valuationsof VM lead to the same system behaviors. The state of M can beobserved through implementing a logger in the system which (e.g.,
periodically) outputs the valuation of VM . Thus, we can obtain aset of finite traces of the system. In the following, we assume thatthe logged variables and the sampling frequency are adequate tocapture the relevant behavior of the system.
We write Σ(VM ) (hereafter Σ for short) to denote D1 × · · · ×
Dn , which is the set of all observable states of M . Note that Σ
may be infinite if there are float variables with infinite domains.
A finite system trace is a sequence π = hs1 , s2 , · · · , sn i wheresi ∈ Σ for all i. In other words, a finite system trace can be seen
as a finite string over Σ. We denote the set of all finite strings
over Σ, including the empty string hi, as Σ? . Given a string t, we
say that a string t0 is a prefix of t if and only if there is a string
t00 ∈ Σ? such that t = t0 · t00 where · denotes string concatenation.
We write prefix (t) to denote the set of all prefixes of t. We denotea system trace with length l by π l and its k -th letter by π[k]. We
also use π[i · · · j] to denote the trace from π[i] to π[j].
System model. Let Σ0 be the set of initial states of system M .
If we impose a prior probability distribution µ0 on the states inΣ0 (e.g., a uniform distribution over all states in Σ0 ), M can beeffectively viewed as a discrete time Markov Chain (DTMC) [11].
Formally,
Definition 1. A DTMC D is a tuple (S, ıinit , P r), where S isa countable, nonempty set ofPstates ; ıinit : S → [0, 1]
is the initial distribution s.t. s∈S ıinit (s) = 1; and P r :S × S → [0, 1] is the transition probability assigned toevery
pair of states which satisfies the following condition:P00s ∈S P r(s, s ) = 1.
An example DTMC is shown in Fig. 2, where states are labeled
for readability. A DTMC induces an underlying digraph wherestates act as vertices and there is an edge from s to s0 if and only
if P r(s, s0 ) > 0. Given a path π = hs1 , s2 , · · · , sn i in D, wewrite P(π, D) = P r(s1 , s2 ) × P r(s2 , s3 ) × · · · × P r(sn−1 , sn )to denote the probability of exhibiting π in D. Furthermore, wewrite Path f in (D) to denote the set of finite paths of D startingwith an initial state, i.e., a state s such that ıinit (s) > 0.
M can be viewed as a DTMC DM = (S, ıinit , P r) whereS = Σ is the states of M ; ıinit = µ0 is the imposed priorprobability distribution of the initial states.
Model learning. Once we obtain a set of system traces from thesystem logger, we can then apply a probabilistic model learningalgorithm to ‘learn’ a DTMC. Most existing model learningalgorithms are inspired by ALERGIA [13], which first transforms
the traces into a prefix tree and then iteratively merges the tree

3

Systemlogs

SafetypropertyModellearning

Predicate
abstraction

Predicateset

Refinement

True

Spurious?

Counterexample

False
Reportcounterexample

PMC

True
Reporttrue

Fig. 1: An overview of our framework

0.98
start

0.01

a

c

0.01
0.5

b

triggered once a violation is detected). The goal of analysis is thus
to show such safety violation is rare (i.e., with low probability).
For instance, in our case study of the water treatment system,a safety property is that the water level in the backwash tankmust be within certain range. Otherwise, a system shutdown
is triggered. Our task is then to show the probability of thewater level being out of the range is low enough such that theprobability of triggering system shutdown is low.

0.9

0.1
0.5

d

1

Fig. 2: An example DTMC
nodes based on whether the two nodes are compatible. Based on
the same idea, a genetic-algorithm based learning algorithm is
proposed in [55] to merge the tree nodes through evolution. We
present one of the latest ALERGIA-style learning algorithms as arepresentative [40], [42] in Section 3.2. With the learned DTMC,
we can verify safety properties by probabilistic model checking.
Probabilistic model checking. Assume that we are given a property in the form of a probabilistic linear temporal logic formula(PLTL) [10], [27]. The syntax of the PLTL is defined as follows.

ϕ ::= p|¬ϕ|ϕ ∧ ϕ|P./r (ϕUϕ)
where p is an atomic proposition constituted by V , r ∈ [0, 1] ⊆R, ./∈ {<, ≤, >, ≥} and U is a modal operator which reads‘until’. The properties of interest in this work is the safety
fragment of PLTL properties. In the following, we focus on theproperty of the form1 : P≤r (Fϕ) where Fϕ is a short form fortrueUϕ. Intuitively, this property states that the probability ofeventually reaching a bad state does not exceed a certain threshold.
For instance, property P≤0.2 (F observe0 > 1) states that theproperty of reaching a state with observe0 > 1 is less than 0.2.
A DTMC D satisfies P≤r (Fϕ) if and only if the accumulated
probability of all paths in Path f in (D) which satisfy Fϕ is lessthan or equal to r. We write D  P≤r (Fϕ) to denote that DTMC
D satisfies P≤r (Fϕ).
The reason that we focus on probabilistic properties is thatsafety-critical CPS are often designed with built-in mechanisms
for handling safety violation (e.g., a shutdown sequence is
1. Recursive PLTL properties are not handled due to the limit of model
learning [42].

Problem Definition. Our problem is then defined as follows.
Given a system M and a property P≤r (Fϕ), how do we check
whether the property is satisfied by M without having its model
D? In case that the property is not satisfied, can we present someevidence , i.e., in the form of counterexamples? In case that theproperty is satisfied, can we present some evidence as well?

3

O UR A PPROACH

Since the system is complicated and a precise system model isunavailable, we cannot apply existing techniques like PMC tocheck whether the property is satisfied or not. One way to solve
the problem is to construct a DTMC model D approximating M
and then verify the given property based on D. There are however
a number of questions that must be answered in order to makethis approach work. First, how do we construct D systematically?
In particular, what are the states in D and what are the transition
probabilities? If we consider every different valuation of variables
VM to be a different state, D is likely to contain many (and
often infinitely many) states. Such D is difficult to learn orverify. We thus would like to construct a small D (with states
more abstract than a valuation of VM ) which would be used toverify the property. Secondly, after constructing D and verifying
the property based on D, how do we quantify the confidence
we have on the verification result, knowing that D may not be
precise? In the following, we present answers of these questions.
For simplicity, we illustrate how our approach works using thefollowing running example (which is motivated by the crowds
protocol [45]).
Example Assume a system where multiple users are browsing
the web (i.e., sending/receiving messages to/from Web servers).
Further assume there are eavesdroppers on the network who
can observe the direct source of a message. In order to provide

4

TABLE 1: Details of the variables in the crowds protocols.
Name

Type

Meaninglaunchnew
runCount
start
run
lastSeengoodbadrecordLast
badObserve
deliverdone
observe0 to observe19

bool
bool
int
bool
bool
int
bool
bool
bool
bool
bool
bool
int

Start modeling?
Initialize a new protocol instance?
Counts protocol instances
Start the protocol?
Run the protocol?
Last crowd member to touch msg
Crowd member is good?
Crowd member is bad?
Record last seen crowd member?
Bad members observes who sent msg?
Deliver message to destination?
Protocol instance finished?
Counters for attackers’ observations

anonymity for the users, a message from a user is not directly sent
to the destination, but rather routed among the users so that theeavesdroppers cannot identify the actual source of the message.
Each user in the system uses a complicated algorithm to decide onwhether to forward a received message to its destination or to someother user on the network. Assume there are a total of u users.
The property to be verified is that the probability of observing amessage sending to its destination by its actual source more thanonce in r runs should not exceed a threshold, say 0.2. Formally,
it is specified as: P≤ 0.2 (F observe0 > 1) where observe0 is
a variable in the system which captures the number of message
sending to its destination by its actual source. Without knowing
how each user decides on forwarding the messages, we cannot
develop a precise model.
3.1

Predicate Abstraction

In our approach, we start with collecting a set of system traces Π,
by introducing a logger in the system and executing the system
multiple times. For instance, in the running example, we log
the valuation of all 32 variables, including where the message
is originated, where it is forwarded to, etc. The details of all
the logged variables are shown in Table 1. The logged tracescontain many details, most of which may not be relevant toverifying the property. Thus, we start with abstracting the traces,
through predicate abstraction [54]. Recall that a concrete trace isa sequence hs0 , s1 , · · · , sn i where si ∈ Σ for all i is a valuationof variables VM . Predicate abstraction is to construct an abstract
trace ha0 , a1 , · · · , an i where, for all i, ai is the valuation of a setof propositions AP given si .
Let BExpr V denote the Boolean expressions over V . A
proposition ψ is a Boolean expression over a set of variables.
For an expression e ∈ Expr V , we denote its valuation in states ∈ Σ by [[e]]s . For a Boolean expression e, [[e]]s ∈ {0, 1}
where 0 stands for false and 1 for true. We write s |= ψ iff[[ψ]]s = 1. We denote the set of states satisfying a predicate ψ by[[ψ]] = {s|s ∈ Σ ∧ s |= ψ}.
Let P = {p1 , · · · , pk } ⊆ BExpr V be a set of propositions
over V . Given a state s ∈ Σ, we define an abstraction function
as: αP (s) = ([[p1 ]]s , · · · , [[pk ]]s ), which maps the state s to an
abstract state, i.e., a bit vector with length k where each bit represents the truth value of a proposition in P . We write ΣP to denotethe set of abstract states with respects to P . Given a logged trace
π = hs1 , s2 , · · · , sn i, we can construct an abstract trace with respect to predicates P as: πP = hαP (s1 ), αP (s2 ), · · · , αP (sn )i.
Let Π be the set of sample traces such that each π ∈ Π is a string

start

hi

100

0

0

100

0

00

100

0

000

1

90
001

0

0000

1

88
0001

1

10

2
0011

8

Fig. 3: Example tree representation of samples
in Σ∗ . We can construct a set of abstract traces ΠP from Π byabstracting each trace in Π one by one.
In our running example, we assume that the set Π contains
two logged traces: h0, 0, 1, 1i and h0, 1, 2, 2i where each number
denotes a value of variable observe0. Note that we have removed
the values of all other 32 variables for simplicity. Based on theabove-mentioned property, we set the initial set of predicates P tobe {observe0 > 1}. After predicate abstraction, we obtain twocorresponding abstract traces: h0, 0, 0, 0i and h0, 0, 1, 1i where anumber 0 means that observe0 ≤ 1 and 1 means observe0 > 1.
3.2

Model Learning

With the set of abstract traces ΠP , we then apply existing model
learning techniques [16], [40], [42], [55] to construct a DTMC
model DP . The essential idea of model learning is to construct
a DTMC DP such that it maximizes the probability of observing
the traces ΠP as well as contains a relatively small number ofstates. Several learning algorithms have been proposed [13], [21],[48], [49], [55]. In the following, we present one of the learningalgorithms called AALERGIA [40], [42] as a representative andremark that our approach can be configured to work with different
learning algorithms, as we show in Section 4.
AALERGIA learning algorithm The AALERGIA algorithm
makes the following assumptions. First, the sample traces are
generated by a system which can be modeled as a DTMC.
Secondly, the sample traces are mutually independent. Thirdly,
the length of each trace is independent from the sequence of statesobserved. The AALERGIA algorithm has been proved to converge
to the actual model if a sufficiently large number of sample traces
are provided [40], [42].
Let prefix (ΠP ) = {prefix (t)|t ∈ ΠP } be the set of all
prefixes of any trace in ΠP . The set of traces ΠP can be naturallyorganized into a tree tree(ΠP ) = (N, root, E) where each nodein N is a member of prefix (ΠP ); the root is the empty string hi;
and E ⊆ N × N is a set of edges such that (π, π 0 ) is in E if andonly if there exists e ∈ Σ such that π · hei = π 0 . For instance,
assume that ΠP in our running example contains 100 abstract
traces: 88 of them are h0, 0, 0, 0i, 2 of them are h0, 0, 0, 1i, 2 ofthem are h0, 0, 1i, and 8 of them are h0, 0, 1, 1i. Fig. 3 shows
the tree representing this set of abstract traces, where each node
represents a prefix of some abstract trace. The state labels are to
be explained later.
The AALERGIA algorithm is inspired by stochastic regular
grammatical inference, which aims to learn the structure of astochastic finite state automaton and estimate its transition probabilities [34]. The idea is to generalize tree(ΠP ) by merging thetree nodes according to certain criteria in certain fixed order. Intuitively, two nodes should be merged if they are likely to represent

5

0

000

1

90

100 → 190 100 → 190 100 → 190

001

start

hi

0

0

0

00

10 → 12

0

0000

1

88
0001

2

1

0011

8

Fig. 4: Merge node 00 and node 000.

the same state in the underlying DTMC. Since by assumption we
do not know the underlying DTMC, whether two nodes should bemerged is heuristically decided through a compatibility test, which
intuitively measures how similar two nodes are. We remark that thecompatibility test effectively controls the degree of generalization.
Different types of compatibility test have been studied [13], [34],[47]. In [13], the compatibility test is based on the Hoeffding
bounds, whereas the DSAI algorithm proposed in [21] uses a
condition based on calculating certain distance between the two
nodes. In the following, we present the compatibility test adopted
in AALERGIA.
First, each node π in tree(ΠP ) is labeled with the numberof traces π 0 in ΠP such that π is a prefix of π 0 . Let L(π)
denotes its label. Two nodes π1 and π2 in tree(ΠP ) are considered compatible if and only if they satisfy two conditions.
The first condition is last(π1 ) = last(π2 ) where last(π) isthe last letter in a string π , i.e., π1 and π2 must agree on
the last abstract state. The second condition is that the future
behaviors from π1 and π2 must be sufficiently similar (i.e., within
Angluin’s bound [8]). Formally, given a node π in tree(ΠP ),we can obtain a probabilistic distribution of the next node bynormalizing the labels of the node and its children. In particular,
for any event e ∈ ΣP , the probability of going from node π to
π · hei, i.e., the probability of observing e after π , is defined as:
P r(π, hei) = L(π·hei)
L(π) . We remark the probability of going fromnode π to itself, i.e., the probabilityof not observing the nextPnode, is P r(π, hi) = 1 − e∈ΣP P r(π, hei). The multi-step
probability from node π to π · π 0 where π 0 = he1 , e2 , · · · , ek i,written as Pr (π, π 0 ), is the product of the one-step probabilities.

P r(π, π 0 ) = Pr (π, he1 i) × Pr (π · he1 i, he2 i)×· · · × Pr (π · he1 , e2 , · · · , ek −1 i, hek i)(1)

Two nodes π1 and π2 are compatible if the following is satisfied:for all π ∈ Σ?P ,q|P r(π1 , π) − Pr (π2 , π)| < 6  log(L(π1 ))/L(π1 )+q(2)
6 log(L(π2 ))/L(π2 )Intuitively, it means that the distribution of future traces from π1
and π2 must be similar. We highlight that  used in Eq. 2 is aparameter which effectively controls the degree of node merging.
Intuitively, a larger  leads to more node merging and subsequently
fewer states in the learned model DP . It is also required that
 should be larger than 1 to guarantee the convergence of thealgorithm.
If π1 and π2 are compatible, the tree is transformed suchthat the incoming edge of π2 is directed to π1 . Next, for any
π ∈ Σ∗P , L(π1 · π) is incremented by L(π2 · π). The algorithm

works by iteratively identifying nodes which are compatible andmerging them until there are no more compatible nodes. The orderof choosing merging candidates is hierarchical: first in order oftree depth and for a given depth in the alphabet order of the last
observation.
Recall that Fig. 3 is the tree representing 100 abstract traces ofour running example. The labels on the nodes are the numbers oftimes the corresponding string is a prefix of some trace in ΠP . For
instance, node hi is labeled with 100 because hi is a prefix of all
traces. This tree can be viewed as the initial learned model which
has no generalization. Next, the tree is generalized by merging
nodes. Assume that node h00i and node h000i in Fig. 3 pass thecompatibility test so that they are to be merged. Firstly, we update
the node label of h00i to be the sum of the numbers labeling h00i
and h000i. Secondly, the numbers labeling decedents of h000i areadded to the corresponding decedent nodes of h00i. The result isshown in Fig. 4, where the numbers after the arrow are the ones
after node merging. For instance, since L(h000i · h1i) is 2, weupdate the label of node h001i from 10 to 12.
After merging all compatible nodes, the last step is to normalize the tree so that it becomes a DTMC DP . In particular, eachnode π is taken as a state in DP . The transition probability from0)
π to a child π 0 is set to be: L(πL(π) and the probability to itself is set
to 1 minus the sum of probabilities to its children accordingly. For
instance, in the example shown in Fig. 4, the probability transiting
12, and the probability to itself
from node h00i to node h001i is 190
12
is 1 − 190 .
Remark 1. Notice that the parameter  in Eq. 2 has an immediate
effect on the compatible test and thus the learned model. One
question would be how to determine the best  for the bestlearning outcome. AALERGIA measures how good a learned
model DP is by the Bayesian Information Criteria (BIC) score.
Intuitively, a learned model which generates the input system
traces ΠP with higher probability and has fewer number ofstates has a higher BIC score. AALERGIA thus automaticallysearches for the best  that has the highest BIC score andoutput the corresponding model [40].
GA-based learning algorithm A genetic-algorithm based learning approach (GA in short hereafter) was proposed in [55]. The
idea is to reduce the problem of model learning to an optimization
problem, i.e., finding an optimal DTMC DP that has the highest
BIC score. GA encodes a chromosome by randomly merging thenodes in the prefix tree and apply mutations and crossover in thestandard way to search for the best model. It has been shown suchan approach could outperform AALERGIA sometimes [55]. We
remark that different model learning approaches can be adopted inthis work.
3.3

Spuriousness Checking

Given the learned DTMC model DP and the property P≤r (Fϕ),
we then use an existing probabilistic model checker (e.g.,
PRISM [38]) to check whether DP |= P≤r (Fϕ). There are twocases.
The first case is that DP |= P≤r (Fϕ) is not satisfied. Since
this verification result is based on the learned model DP , it may
not be correct according to M . Thus, we must validate this result
based on the actual system. To do so, we construct a probabilistic
counterexample and check whether the counterexample is spurious. In general, a probabilistic counterexample is in the form of

6a tree [26]. Since we assume that our property is in the form ofP≤r (Fϕ), we define it to be a set of abstract paths of DP for
simplicity.
Definition 2. Given a DTMC DP and a property P≤r (Fϕ),
a counterexample is a set C ⊆ PathP
f in (DP ) such that
last(π) |= ϕ for every path π in C , and π∈C P(π, DP ) >r.
Intuitively, a probabilistic counterexample for P≤r (Fϕ) is a setof finite paths in DP whose accumulated probability is larger thanr. There are existing approaches to construct such counterexamples [26]. In our setting, because DP is learned based on a set of
abstract traces, a probabilistic counterexample may be spurious.
A probabilistic counterexample C is spurious if and only if theprobability measure of the concrete paths of M corresponding to
C is less than r. Given an abstract path π = ha1 , a2 , · · · , an i ∈P athf in (DP ), we write γ(π) to denote the set of concrete paths{hs1 , s2 , · · · , sn i ∈ P athf in (M )|∀i. αP (si ) = ai } whichbecome π after predicate abstraction using P . We write γ(C) todenote the set of corresponding concrete paths: {π 0 |∃π ∈ C, π 0 ∈γ(π)}.
Definition 3. Given the system M , a DTMC DP , a propertyP≤r (Fϕ) and a counterexample C in terms of DP andP≤r
P(Fϕ), C is a spurious counterexample of M if and only
if π∈γ(C) P(π, M ) ≤ r.
Recall that M can be viewed as a DTMC and P(π, M ) is
the probability of path π in M . The above notion of spurious
counterexample is a special case of that of probabilistic automaton
defined in [31]. Checking whether a probabilistic counterexample
C is spurious or not in our setting is however more challenging
than that in the setting of [31]. The reason is that we do not havea model of M and thus the probability of a concrete path in M
cannot be calculated. Our solution is to
Padopt hypothesis testing [58] to test whether the hypothesis π∈γ(C) P(π, M ) > r
holds given certain error bounds. If it does, we report the counterexample to the user together with the error bounds. Otherwise,
we conclude that it is a spurious counterexample and proceed to
the next step, i.e., abstraction refinement.
In the following, we briefly introduce how hypothesis testing isused for spuriousness checking. Hypothesis testing is a statisticalprocess to decide the truthfulness of two mutual exclusive statements. One is H0 : theP null hypothesis that the counterexample
is not spurious, i.e., π∈γ(C) P(π, M ) > r. The other is H1 :the alternative
hypothesis that the counterexample is spurious,
P
i.e.,
P(π,
M ) ≤ r. The probability of making anπ∈γ(C)
error is bounded by (α, β), such that the probability of a TypeI (respectively, a Type-II) error, which rejects H0 (respectively,
H1 ) while H0 (respectively, H1 ) holds, is less or equal to α
(respectively, β ). The test needs to be relaxed with a confidence
interval (r − δ, r + δ), where neither hypothesis is rejected andthe test continues to bound both types of errors [39]. In practice,
the parameters (i.e., (α, β), and δ ) can often be decided by how
much testing resources are available. In general, more resource isrequired for a smaller error bound.
Hypothesis testing works by keeping sampling traces from
M until a stopping condition is satisfied. There are two main
methods to decide when sampling can be stopped. One is fixedsize sampling test, which requires running all the predefined

number of tests. One difficulty of this approach is to find theappropriate number of tests to be performed such that the error
bounds are valid [39]. In this work, we adopt the alternative
approach, which is sequential probability ratio test (SPRT). SPRT
dynamically decides whether to reject or not a hypothesis every
time we obtain a new trace, which yields a variable sample size.
SPRT is usually faster than fixed-size sampling test as the testingprocess ends as soon as a conclusion is made. In the following, we
briefly introduce how SPRT works and readers can refer to [39]for details.
The basic idea of SPRT is to calculate the probability ratio
each time after observing a trace and evaluate two stopping
conditions [9]. If either of the conditions is satisfied, the testing
stops and returns which hypothesis is rejected. Let n be thenumber of sampled traces so far, the decision is based on thefollowing probability ratio:nY
p1n
P (Bi = bi |p = p1 )
pdn (1 − p1 )n−dn
=
= 1dn
p0n
P (Bi = bi |p = p0 )p0 (1 − p0 )n−dn
i=1

(3)

, where p1 = r + δ , p0 = r − δ , Bi is a random variable withboolean values representing whether a new sampled trace is in the
counterexample (1 if yes and 0 otherwise), dn is the number ofsampled trace which are in the counterexample. We will accept
p1n
βH0 (reject H1 ) if pp1n
≥ 1−βα and H1 (reject H0 ) if p0n ≤ 1−α .
0nOtherwise, SPRT continues sampling until either H0 or H1 isrejected. We remark that SPRT is guaranteed to terminate withprobability 1 [9].
In our running example, hypothesis testing is done by repeatedly generating messages from some user in the network andobserve the resultant traces. Assume there are now a total ofn traces in Π (including the ones obtained initially) and b ofthem are in γ(C). We can then calculate whether to accept H0
or H1 based on n and b in the standard way. If neither can be
accepted, we continue sampling and updating n and b until oneof the hypothesis is accepted. The following theorem follows thecorrectness of hypothesis testing immediately.
Theorem 1. If LAR reports a counterexample, the probability of
M satisfying the property is ‘bounded’ by β .
Proof 1. Notice that if the counterexample is not spurious, then theproperty is violated by the system. So the probability that M
satisfies the property is no larger than the probability that thecounterexample is actually spurious while a counterexample isreported, which is the Type-II error bounded by β .
In the case that the model checker confirms that DP |= P≤r (Fϕ),
it is guaranteed that the the original system M satisfies theproperty if an unbounded number of traces are used for learning.
Theorem 2. If Π has an unbounded number of traces, DP |=P≤r (Fϕ) with probability 1 only if M satisfies the property.
Proof 2. The proof of the theorem is as follows. First, theAALERGIA algorithm eventually converges to the actual
underlying DTMC [40], [42] with probability 1, which is aquotient automaton of the original model M (with respect tothe predicate abstraction). Second, it is established in [31] thatthe quotient automaton simulates the original system M . Thus,
it is safe to conclude that M satisfies the property if its quotient
automaton does.

7
0.998

start

0

0.986

1
0.002

1

start

1

01

10

0.002

Fig. 5: Illustration of broken paths

9970

start

However, the number of traces in Π is often limited in practiceand there is no guarantee that the learned model DP has converged
to a model which simulates M . Our remedy to this problem isthat we present the model DP as a part of the verification result.
That is, we report that the property is satisfied by the system,
provided that DP is a correct model of the system. We remarkthat because there is no precise system model, our goal is not
to completely verify the system. Rather, our goal is to provide
evidence (a counterexample or a model) with confidence on why
we believe that the verification result is sound. If we would like tohave certain confidence on the “correctness” of the learned model
DP , one way is to make sure that the number of traces in Π
satisfies certain constraints. We skip the details as this is beyond
the scope of this work. A discussion on the number of samples
required to guarantee that the difference between the transition
probabilities of DP and M is given in Appendix A.
3.4

Refinement

If the counterexample C is spurious after hypothesis testing, theabstract model DP is to be refined so as to rule out the spurious
counterexample. Following the idea of CEGAR [18], [31], this isachieved by identifying a new predicate for predicate abstraction.
Due to the lack of a system model, standard methods for generating new predicates (e.g., weakest pre-condition calculation [18] orinterpolation [29]) are infeasible in our setting. We thus adopt
techniques from the machine learning community to solve theproblem.
Identify spurious transitions The first step of identifying a new
predicate is to identify spurious transitions in the counterexample.
Fundamentally, spuriousness is the result of an inappropriate levelof abstraction. Fig. 5 shows how abstraction could induce moreprobability measure over abstract paths, due to broken paths [35].
The probability of paths in the counterexample C may be inflated.
Intuitively, if a probabilistic counterexample C is spurious, there
must be at least one path π in C whose probability is inflated,i.e., π has certain probability d in DP , whereas the accumulated
probability of γ(π) in M is less than d. Furthermore, there mustbe at least one transition in π whose probability in DP is higher
than the accumulated probability of the corresponding concrete
transitions in M . The idea is then: if we are able to identify such
an abstract path π and such a transition in π , we could refine DPsuch that the transition is no longer associated with the inflated
probability so that C may no longer be a counterexample. In thefollowing, we define such transitions and later use them to find
new predicates.
Formally, let C = {π1 , π2 , · · · , πn } be a spurious probabilistic counterexample. Let hs, s0 i be a pair of consecutive states
which form a transition of a path πi in C . Let γ(s) denote theset of concrete states in M which become s after abstraction,i.e., γ(s) = {x ∈ Σ|[[x]]P = s}, and |γ(s)| denote the0numberP of concrete states in γ(s). We write P(hs, s i, M ) tobe s0 ∈γ(s),s0 ∈γ(s0 ) #(hs0 , s00 i, M )/|γ(s)|, i.e., the probability0of having a corresponding concrete transition in M . hs, s0 i is

0

30
30

1

0.012
00

0.03
1

11

0.97

Fig. 6: Identify a most spurious transition
called a spurious transition if P(hs, s0 i, DP ) > P(hs, s0 i, M ).
Since we do not have the model M , it is impossible to computeP(hs, s0 i, M ). Rather, we estimate it based on Π (which now
contains all traces sampled during the hypothesis testing in theprevious step). That is, given the set of sample traces Π, we estimate P(hs, s0 i, M ) by #hs, s0 i/#s where #hs, s0 i is the numberof times the transitions take place and #s is the number of times s
is visited. Next, we identify the most spurious transition for refinement, i.e., the transition hs, s0 i s.t. P(hs, s0 i, DP ) − #hs, s0 i/#s
is the largest of all transitions.
Algorithm 1 gives a detailed description on how we identify
the most spurious transitions. We first collect all the transitions in
the learned model DP at line 1. Then we iterate through all thetransitions at line 4. For each transition, we apply Algorithm 2 toobtain #s and #hs, s0 i. The basic idea is to check all the tracesin Π and count how many times we observe an abstract state s
and a transition hs, s0 i. We then calculate the difference between
P(hs, s0 i, DP ) − #hs, s0 i/#s at line 7. After iterating through all
the transitions, we sort them in descending order according to thedifference at line 11 and return the sorted transitions at line 12.
Fig. 6 shows the first learned model DP of our running
example on the top-left, where there are two states 0 and 1 representing the state observe0 ≤ 1 and observe0 > 1 respectively.
There are in total three transitions: h0, 0i , h0, 1i, h1, 1i. Basedon the learned model, P(h0, 0i, DP ) is 0.998; P(h0, 1i, DP )is 0.002 and P(h1, 1i, DP ) is 1. Assume that the estimationof P(h0, 0i, M ) is 0.997; the estimation of P(h0, 1i, M ) is
0.003; and the estimation of P(h1, 1i, M ) is 1. By calculating
the difference between the transition in the learned model andits estimation, we find that the transition h0, 0i has the largest
difference (i.e., the most spurious), which is used for abstraction
refinement.
Remark 2. We remark that the identified spurious transitions may
be different if two different counterexamples are provided.
Note that we follow the approach in [26], which calculatesa smallest counterexample, i.e., a minimum set of paths toform a counterexample.
Labeled data collection Next, we identify a new predicate basedon the most spurious transition hs, s0 i. Intuitively, the reason thatthe transition is spurious is that many abstract paths in DP going
through this transition are infeasible. This is illustrated in Fig. 5,
where a number of paths are ‘broken’ at the middle state. Notethat each abstract state in DP groups a set of concrete states in Σ.
Intuitively, hs, s0 i is spurious because s groups some states whichcannot transit to any concrete states in s0 , with states which can.
As a result, the probability of transiting from s to s0 is inflated.
Thus, in order to prune the spurious counterexample, we need torefine the model such that s is split in a way such that the states
which cannot transit to any concrete states in s0 are separated from

8

Collect all the transitions Trans in DP ;Let PDiffs be the array storing the probability differences;
3 Let ATrans be the set of analyzed transitions andinitialized to be empty;
4 while Trans! = ∅ do
5
Randomly pick a transition Tran = hs, s0 i from Trans;
6
Apply Algorithm 2 CountTran(Tran, Π, P ) to get #s
and #hs, s0 i ;7Calculate Pdiff as the difference between #hs, s0 i/#s
and the transition probability of hs, s0 i in DP ;8
Add Pdiff to PDiffs ;9
Add Tran to ATrans;
10
Remove Tran from Trans;
11
12

Abstraction

1

2

D−

D+

Algorithm 1: IdentifyST(Π, DP , P )
s1

s2

X

0

0

s3

X

s4

X

0

0

7

s5

···

1

···

Fig. 7: Labeled data collection at spurious transition h0, 0i+<latexit sha1_base64="ypaUeMtKML39Ecmqzd7qk0L91y0=">AAACB3icbVDLSsNAFJ3UV62vqEtBgkWoWEoigi6LunAZwT6giWEynbZDZyZhZiKUkJ0bf8WNC0Xc+gvu/BsnbRZaPXDhcM693HtPGFMilW1/GaWFxaXllfJqZW19Y3PL3N5pyygRCLdQRCPRDaHElHDcUkRR3I0FhiykuBOOL3O/c4+FJBG/VZMY+wwOORkQBJWWAnPfG0LG4F16nNU8BtVIsFRm9avArXsuOQrMqt2wp7D+EqcgVVDADcxPrx+hhGGuEIVS9hw7Vn4KhSKI4qziJRLHEI3hEPc05ZBh6afTPzLrUCt9axAJXVxZU/XnRAqZlBMW6s78VDnv5eJ/Xi9Rg3M/JTxOFOZotmiQUEtFVh6K1ScCI0UnmkAkiL7VQiMoIFI6uooOwZl/+S9pnzQcu+HcnFabF0UcZbAHDkANOOAMNME1cEELIPAAnsALeDUejWfjzXiftZaMYmYX/ILx8Q3+RZi4</latexit>(s, DP , ⇧)support vectors

Sort ATrans according to PDiffs in descending order;
return ATrans

Algorithm 2: CountTran(hs, s0 i, Π, P )for every path π ∈ Π do
Abstract π using P to get the abstract path πP ;3
Let l be the length of π ;4
for si ∈ πP [2 · · · l] do
5if πP [i − 1] = s then6#s = #s + 1;
7
if DP (πP [i − 1], πP [i]) = s0 then8#s0 = #s0 + 1;
9
Add the corresponding concrete state ofπP [i − 1] to γ + (s, DP , Π);

1

2

10
11

12

else
Add the corresponding concrete state ofπP [i − 1] to γ − (s, DP , Π);return #s, #hs, s0 i, γ + (s, DP , Π), γ − (s, DP , Π)

the rest. In the following, we first collect these two sets of statesand identify a predicate for separating them using a classification
algorithm.
Given any concrete execution π = hs1 , s2 , · · · , sn i in Π, it isclear that we can map any state si in the sequence to an abstractstate in DP . Let γ(s, DP , Π) be the set of concrete states in any
execution in Π which are mapped to state s in DP . We define
γ + (s, DP , Π) = {x|x ∈ γ(s, DP , Π) ∧ ∃h· · · , x, y, · · · i ∈Π ∧ y ∈ γ(s0 , DP , Π)}, i.e., the set of concrete states in s which
do transit to a concrete state in s0 in one of the concrete trace.
We define γ − (s, DP , Π) to be γ(s, DP , Π) − γ + (s, DP , Π).
Algorithm 2 shows how we collect the positive and negative datafrom system traces for a given spurious transition. For every tracein Π, we first abstract π with P at line 2. Starting from thesecond state in πP to the end, we iteratively check whether its
previous state is s at line 5. If it is true, we then check whether
the current state is s0 at line 7. If yes, we add the current stateto γ + (s, DP , Π) at line 9; otherwise, we add it to γ − (s, DP , Π)instead. Fig. 7 illustrates how the above works with our running
example. Assume that at the top is a concrete trace and at thebottom is the corresponding abstract trace. Given that we identified
previously that the spurious transition is h0, 0i, the concrete statess1 , s2 and s3 are collected to the set γ + (s, DP , Π) and state s4<latexit sha1_base64="fMAc8tpbghrDlu9wViry3E39xrI=">AAACB3icbVDLSsNAFJ3UV62vqEtBgkWoUEsigi6LunAZwT6giWEynbZDZyZhZiKUkJ0bf8WNC0Xc+gvu/BsnbRZaPXDhcM693HtPGFMilW1/GaWFxaXllfJqZW19Y3PL3N5pyygRCLdQRCPRDaHElHDcUkRR3I0FhiykuBOOL3O/c4+FJBG/VZMY+wwOORkQBJWWAnPfG0LG4F16nNU8BtVIsFRm9avArXsuOQrMqt2wp7D+EqcgVVDADcxPrx+hhGGuEIVS9hw7Vn4KhSKI4qziJRLHEI3hEPc05ZBh6afTPzLrUCt9axAJXVxZU/XnRAqZlBMW6s78VDnv5eJ/Xi9Rg3M/JTxOFOZotmiQUEtFVh6K1ScCI0UnmkAkiL7VQiMoIFI6uooOwZl/+S9pnzQcu+HcnFabF0UcZbAHDkANOOAMNME1cEELIPAAnsALeDUejWfjzXiftZaMYmYX/ILx8Q0Bhpi6</latexit>(s, DP , ⇧)classifierFig. 8: A simple example of SVM with only two variables. The
filled circles are the collected positive states and the empty circles
are collected negative states.
is collected into γ − (s, DP , Π).
Generate a new predicate Once we obtain the labeled data of
the spurious transition, we then adopt a supervised classification
technique to generate a new predicate for refinement. In particular, we use Support Vector Machine (SVM) [15], [20] as itis reasonably scalable and produces a classifier in the form ofa predicate. SVM is a supervised machine learning algorithm
for classification and regression analysis. In this work, we use
its binary classification functionality. Mathematically speaking,the binary classification functionality of (linear) SVM works asfollows. Given the two sets of concrete states γ + (s, DP , Π) andγ − (s, DP , Π), SVM generates, ifPthere is any, a linear classifier(hyperplane) in the form of e = i ci ∗ xi ≥ c where xi ∈ V
is a variable value and ci and c are learned coefficients such that(1) for every state x ∈ γ + (s, DP , Π), [[e]]x = 1 and (2) for every
state x ∈ γ − (s, DP , Π), [[e]]x = 0. As a simple example, fora classification task with only two features (variables), a linear
classifier (hyperplane) is a line that linearly separates the two setsof data while providing a maximum margin between the two sets,
which is shown in Fig. 8.
In our running example, since transition h0, 0i is the most
spurious, we collect the two sets of concrete states in order tosplit state 0 in the DTMC shown on the left of Fig. 6. Recall
that a concrete state contains the valuation of 32 variables. We
feed the two sets into SVM to generate a classifier. Notice that aboolean variable is mapped to 1 if its value is true and 0 otherwise.
The result is a predicate constituted by all 32 variables. To
simplify the predicate, we start from the variable with the largest
coefficient and try to identify a classifier with a minimum numberof variables [20], e.g., a predicate constituted by a minimum
number of variables and yet is able to classify the two sets. The
result is the predicate new < runCount. The predicate is then

9

Algorithm 3: LAR(Π, P≤r (Fϕ), max , α, β, δ)
let P be the set of atomic propositions in ϕ;while true do
3
construct abstract executions ΠP based on Π and P ;4apply a model learning algorithm (e.g. AALERGIA
with  ranging from 1 to max ) to learn a model DP
based on ΠP ;5
probabilistic model check DP against ϕ;
6
if DP |= ϕ then7
report ϕ is verified, model DP ;8
return;

1
2

9

10

11
12

13
14
15
16

17

construct a probabilistic counterexample C using theapproach in [26];run hypothesis testing on C with error bounds (α, β)and indifference region δ ;if C is not spurious thenreport ϕ is violated and the probability of error isbounded by (α, β);return;identify the most spurious transitions hs, s0 i in C ;collect γ + (s, DP , Π) and γ − (s, DP , Π);apply SVM to identify a predicate p separating thetwo sets;
add p into P ;hypothesis testing at line 10. If it passes the test, it is returned asa counterexample. In addition, we output the bounded probabilityof C being a spurious counterexample. Otherwise, at line 14, we
identify the most spurious transition and obtain a new predicate
at line 16. After adding the new predicate into P , we restart theprocess from line 2.
In our running example, after adding the new predicate, welearn the model as shown on the right of Fig. 6. Note that state
0 in the model on the left is split into two states 00 and 01. Thisis due to the new predicate. Note also that the spurious transition
h0, 0i is split into two, which effectively reduces the probability of
the counterexample. Verifying this new model against the property
using PMC returns true and thus we successfully verify the system
without requiring a system model as input.
Remark 4. It is hard to analyze the complexity of LAR as it depends on several factors, i.e., the initial set of predicates P , thecomplexity of the model learning algorithm, the complexity of
hypothesis testing, the complexity of SVM, and whether there
is a linear classifier, etc. We thus rely on empirical studies toevaluate the efficiency and effectiveness of the algorithm inthe next section. Note that if SVM fails to find a classifier for
all the spurious transitions, Algorithm 3 terminates and reports
the verification is unsuccessful. Otherwise, it either reports true
with a supporting model or a counterexample.

4
added into P , and used to refine the abstraction. The right part of
Fig. 6 shows the learned model after refinement, where the second
bit of the state label captures the value of the new predicate. It
can be observed that a new terminal state 00 is introduced, which
effectively reduces the probability of reaching observe0 > 1.
Remark 3. We remark that γ + (s, DP , Π) and γ − (s, DP , Π) may
not be linearly separable, in which case linear SVM could not
generate a satisfactory linear classifier (i.e., the obtained classifier has low classification accuracy). Although SVM could
adopt different kinds of kernels (e.g., polynomial and RBF) to
identify a polynomial or even more expressive classifier, we
prefer linear classifiers as the learned classifier and model arepresented as a part of the verification results and the easier
it is, the easier it is for human understanding. In case a linear
classifier for separating γ + (s, DP , Π) and γ − (s, DP , Π) does
not exist, we move on to identify a predicate using the same
approach based on the next most spurious transition.
3.5

Overall Algorithm

The overall algorithm is shown as Algorithm 3. The inputs of
the algorithms are a set of concrete executions Π, a property
in the form of P≤r (Fϕ), and the parameters (α, β) and δ forhypothesis testing. During each iteration of the loop from line 2
to 17, we start with constructing a set of abstract traces basedon Π and a set of predicates P . Note that we set the initial setof predicates for abstraction to be the set of propositions in theproperty. Next, an abstract DTMC DP is learned using a model
learning algorithm. We then verify DP against the property using
PMC. If the property is verified, we conclude that the system isverified and present DP as a part of the evidence. Otherwise, weconstruct a probabilistic counterexample C (i.e., a set of abstract
paths) at line 9. The spuriousness of C is then checked throughE VALUATION

Our approach has been implemented as a self-contained toolkit
named LAR (available at GitHub [1]) with about 6K lines of Java
code. LAR relies on the LIBSVM library [6], [15] for generating
new predicates and PRISM model checker for PMC [38]. All
models and detailed results discussed below are available at [2].
Experiment settings
We identify and compare our approach with two latest state-of-theart approaches developed based on stochastic regular grammaticalinference. One is the AALERGIA algorithm (hereafter AA) [40],[42]. The other is the GA-based approach (hereafter GA) in [55].
Our test subjects include DTMC models from the PRISM
benchmark suite [36], as well as a real-world water treatment
system (SWaT) [3]. Table 2 summarizes the system configurationand the property to verify of the test subjects, where the detailed
description of the PRISM benchmark systems can be found at [37].
SWaT [3] is a complicated system which involves a series ofwater treatment processes like ultra-filtration, chemical dosing,dechlorination through an ultraviolet system, etc. We regard SWaT
as a representative of our target complex systems. We conduct ourexperiments on a simulator of the SWaT due to safety concerns.
The simulator contains an exact Python translation (about 3K
LOC) of the control software in SWaT and a set of Ordinary
Differential Equations (ODEs) for simulating the environment.
The property we verify is how likely the raw water tank in thesystem would go underflow. For each model, a set of system
traces are first obtained through random simulation. For a faircomparison, we use the same set of system traces to learn fromfor all the algorithms. The total length of the traces for all thesystems is set to be 20000. To validate the verification results,
we need to know the actual results (last column of Table 2). For
each benchmark in the PRISM benchmark suite [36], we apply
PRISM on their corresponding PRISM model to obtain the actual
probability. Since we do not have the actual model of SWaT, we

10

TABLE 2: Case studies under evaluation. Column ‘Config’ is thesystem configuration; column ‘Property’ is the property to verify;
column ‘#states’ is the state space of the original system; column‘Pact ’ is the actual probability of the property being satisfied.
Case study(parameters)

ConfigProperty#statesPactcrowds
(R,S)

5,5
5,10
5,15
5,20

Positive

8k
111k
592k
2062k

0.14580.10480.09220.0861

2,5

egl
(L,N)

2,10

Unfair for A
Unfair for B
Unfair for A
Unfair for B

0.51560.48440.50050.4995

29k
6E5k

nand
(N,K)

20,2
20,3
60,1
60,3

Reliable

155k
232k
4717k
1.4E5k

0.41290.46850.26950.6377

SW aT
(S,R)

5,1
5,5
10,5

Underflow∞∞∞

0.17130.13890.3333

TABLE 3: Parameters for each algorithm.
Algorithm

Parameter

Value

AA

max

64

GA

number of chromosome
maximum generation
mutation rate
selection probability

50
10
0.1
0.9

α
β
σ

0.05
0.05
0.05
64
0.8

LAR

max
ς

estimate the verification result based on a large number of traces(e.g., one week’s simulation). For each model, LAR is set to verify
a property of the form P≤r (Fϕ). In our experiment, r is set to be
20% above the actual P(Fϕ).
Table 3 shows the details of the parameters we used in our
experiments for AA, GA and LAR respectively. For AA, there
is only one parameter which is the maximum value of  tochoose from2 . For GA, there are 4 parameters as follows. We
set the number of chromosomes in each generation to be 50. The
mutation rate for the mutation operator is set to be 0.1. We use
the tournament selection strategy to select the good chromosomesin each generation and the probability to keep the winner is set
to be 0.9. Finally, the maximum number of generation for theevolution is set to be 10. For LAR, the parameters are mainly
for hypothesis testing, the maximum value of  for AA, and theminimum classification accuracy for SVM. In particular, the error
bounds for hypothesis testing are set as α = 0.05, β = 0.05. The
indifference region is set to be σ = 0.05. The maximum valueof  to choose from is set to be 64 which is the same as AA.
The minimum required accuracy for SVM classification ς is set tobe 0.8. All the experiments were conducted on an OS X machinewith 2.6GHz quad-core Intel Core i7 processor and 8 GB RAM.
We aim to answer the following research questions through ourexperiments.
2. Note that the minimum value is 1 as required for convergence

RQ1: Is LAR better in verifying systems than state-of-the-art
approaches based on learning probabilistic models?
The results are summarized in Table 4, where - means no results
after the preset timeout 2 hours. We show the results of applying
AA and GA on the basic abstraction which is defined by whether
a state satisfies the target property or not in column ‘AA Basic’and ‘GA Basic’ respectively. We can observe that in all cases
the verification results on the learned models are 1 due to overly
coarse abstraction and inappropriate state merging. Column ‘AA’shows the results of the AALERGIA algorithm and column ‘GA’shows the results of the GA-based approach. Column ‘LAR’
shows our results. We leave the explanation of column ‘AALAR’ later. Note that for crowds and nand protocol, we haveto do manual abstraction first for AA and GA, i.e., heuristicallyselect a smallest number of variables which gives us reasonable
results, otherwise neither AA nor GA can learn a model within
the time limit. This means that LAR is competing with AA and
GA combining some manual abstraction. We remark that this isprecisely the advantage of LAR which automatically identifies alevel of abstraction which verifies the property.
It can be observed that LAR successfully verified all systems,
whereas both AA and GA failed on about half the systems. In
most cases especially for the benchmark systems, LAR only takes
few iterations to identify a model which allows us to prove theproperty. This is particularly useful in verifying systems with alarge number of (or infinite) states. For instance, for the egl model,
while AA (or GA) fails to learn or verify any of the 4 cases, LAR
successfully verifies all of them in about 5 seconds and the learned
models have 4 states only. The latter two crowds cases show
similar results. This is especially the case for the SWaT system.
Because the variables in this system are all float numbers, without
abstraction, every logged state is different from others and as aresult, there is no generalization (i.e., no state merging in AA andGA) and no models could be learned. On the other hand, LAR
is able to learn reasonably small models by automatic abstraction
refinement.
Efficiency-wise, Fig. 9 shows the time cost of AA, GA and
LAR for different systems. We can observe that LAR takes muchless time than AA and GA (given the same number of traces).
In over half of the cases neither AA nor GA can learn a model
within the time limit, whereas LAR can learn an accurate model
within minutes. This is largely because a much smaller DTMC islearned, since the abstract traces only have a few symbols (upto 2#P where #P is the number of predicates in P ) in thealphabet. Furthermore, because the learned model is small, model
checking whether the model satisfies the property through PMC
takes much less time. Fig. 10 shows the time distribution of eachstep in LAR, which include learning the model (Learning), PMC
on the learned model (PMC), hypothesis testing of counterexample(Hypothesis testing) and abstraction refinement (Refinement) togenerate a new predicate. A close look reveals that learning, PMC
and spuriousness checking through hypothesis testing dominates
LAR’s time (about 80% on average), while abstraction refinementtakes very little time, i.e., mostly less than 10%. Fig. 11 shows thetime cost of LAR in each iteration. It can be observed that in mostcases the time cost grows slowly by iteration. The only exception
is the last iteration of swat-2. We observe that there is a significant
increase in the number of states in the learned model in the last
iteration, which takes a relatively long time to model check. We
thus have the following answer to RQ1.

11

TABLE 4: Verification results on learned models using different learning approaches.
System#ConfigPactcrowds12
3
40.14580.10480.09220.0861

1
egl

2

nand

SW aT

0.51560.48440.50050.4995AA Basic#states resultAA#statesresultGA Basic#states result#statesGA
resultiters

LAR#statesresult0.15490.101
0.066
0.0877

4
4
4
4

1
1
1
1

10572
10894
-

1
1
-

3
3
3
3

1
1
1
1

102
158
206
266

1
0.1054
1
1

2
2
2
2

6
6
6
6

4

1

-

-

3

1

-

-

1

34

4

1

-

-

3

1

-

-

1

4

0.49610.50390.46190.5381

AA-LAR#statesresult
5
5
5
5
55
107

0.156
0.114
0.082
0.084
0.48340.5166
0.48880.51121
2
3
40.41290.46850.26950.6377

4
4
4
4

1
1
1
1

1257
1793
14987
-

0.48780.49950.1428
-

3
3
3
3

1
1
1
1

90
90
250
-

0.49990.49950.1707
-

3
3
2
4

8
8
6
11

0.38440.53320.1458
0.606

7
7
5
9

0.38490.43
0.22860.6

1
2
3

0.17130.13890.3333

101
186
255

1
1
1

-

-

3
2
3

1
1
1

-

-

7
12
20

274
930
974

0.2
0.14080.2268

852
4139
4226

0.2
0.189
0.2999TABLE 5: Experiment results of LAR: given different safety threshold in the property
System#ConfigPactcrowds12
3
40.14580.10480.09220.08611egl

20.51560.48440.50050.4844

LAR-r2
iters time

result#states

6
6
6
6

2
2
2
2

109
119
114
116

0.17230.10440.063
0.0845

34

1

5

4

1

6

#states

0.49610.50390.46190.5381

LAR-r3iters time

result#states

6
6
6
6

2
2
2
2

104
119
110
115

0.15990.10510.05940.0813

34

1

5

4

1

6

0.49610.50390.46190.5381

LAR-r4iters time

result

6
6
6
6

2
2
2
2

96
108
104
121

0.17940.1051
0.05610.0848

34

1

5

4

1

6

0.49610.50390.46190.5381

nand

1
2
3
4

0.41290.46850.26950.6377

8
8
6
11

3
3
2
4

119
0.6
100
166

0.4532
0.49120.1276
0.381

8
8
6
–

3
3
2
–

95
88
80
–

0.36740.50980.1333
–

8
8
6
–

3
3
2
–

83
60
76
–

0.349
0.49970.1818
–

SW aT

1
2
3

0.17130.13890.3333

274
693
910

7
11
17

48
121
719

0.2
0.22890.4475

204
542
910

6
9
17

40
84
738

0.375
0.39320.4475

204
532
910

6
7
17

41
56
723

0.375
0.42260.4475

Answer to RQ1: LAR is more effective and efficient in verifying complex systems than state-of-the-art approaches basedon learning probabilistic models by automatically identifying
a right level of abstraction for learning.

RQ2: Is LAR able to learn models better than those learned
by state-of-the-art approaches?
Recall that if LAR reports that the property is verified, a model isreturned. It is thus important that the learned models are of highquality. In the following, we evaluate the quality of the learned
models in three aspects.
First of all, it can be observed from Table 4 that the models
generated by LAR have much fewer states than AA or GA, i.e.,
often order of magnitudes fewer than the model learned by AA.
The reason is that we always start with learning based on thecoarsest abstraction and only add one predicate for abstraction if
necessary. We remark that learning small models is important if
the models are to be reviewed by experts or used to implement
runtime monitors as they are easier to interpret. For instance,
for the example crowds protocol, the learned new predicate is
new < runCount, where runCount is a variable representing
how many runs are left and new represents whether it is about tostart a new run. Intuitively, this predicate allows us to separate
the last run from the other runs, which is relevant because if
observer0 is 0 after the second last run, it is impossible to reacha state satisfying observe0 > 1. With the learned predicate, we
can easily interpret the learned system models and implement aruntime monitor monitoring how the system evolves afterwards.
Secondly, to evaluate the accuracy of the learned models, we apply
PMC on the model learned by LAR to compute the probability
P(Fϕ) (although LAR’s verification results are either true or
false). It can be observed that the models produced by LAR
often (i.e., in 14 out of 15 cases) have more or equally precise
verification results than those models learned by both AA and GA.
Lastly, we measure how accurate LAR’s models are, compared to‘best’ model which can be learned at the learned abstract level. To
do that we generate a large number of traces (5 times more thanthose used in LAR), abstract them with the same set of predicateslearned by LAR, and apply AA to learn a model. Given that AA isguaranteed to converge [40], [42], we assume these models to be
the accurate models at this abstract level. We then compare themwith LAR’s models. Column ‘AA-LAR’ shows details related tothese accurate models learned by AA, i.e., the number of states
and the result of P(Fϕ) based on the models. It can be observedthat the models learned by LAR are rather close to these best12Time distribution of LAR in each step

Learning time of AA, GA and LAR
1215

swat-3swat-2163

swat-1

50

7200
7200
7200
7200
7200
7200

nand-4207

nand-390

nand-2

121

nand-1

135

7200
7200

731

egl-2

6

egl-1

5

crowd-3

116

crowd-2

118

crowd-1

110

742

0

7200

578

crowds-4
crowds-3
crowds-2
crowds-1

7200

472

600

nand-4nand-1

1304

7200
7200
116

swat-1nand-2

4790

7200
7200

crowd-4swat-2nand-3

5689
5997
620

swat-3

0% 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%

7200

Learning

PMC

Hypothesis testing

Refinement

1346

2000

4000
LAR

GA

6000

8000

Fig. 10: The time distribution of LAR in each step including
learning, PMC, hypothesis testing and refinement.

AATime distribution of LAR in each iteration

Fig. 9: Learning time of AA, GA and LAR in seconds. The preset
timeout is 7200 s.

120

models. It thus suggests that not only LAR has found an abstractlevel to prove the property but also it is able to learn accurate
models at the chosen abstract level. We thus have the following
answer to RQ2.

Time in seconds

100
80
60
40
20

Answer to RQ2: LAR is able to learn more accurate andmuch smaller models (at the identified abstraction level) thanstate-of-the-art approaches.

0
1

2

3

4
nand-1swat-1

RQ3: Is LAR able to learn models in a property-guided way?
Recall that LAR aims to learn a model which is sufficiently
accurate to show that the probability of reaching certain statesis less than r. Thus, with a larger r, ideally a coarser model whichis easier to comprehend will be learned. In the above experiments,
we fix r to be 20% more than the actual probability. In thefollowing, we perform additional experiments to show the effectof having different r values. That is, we run r which are 40%, 80%
and 100% above the actual probability (for SWaT configuration 1
and 2, we run r which are 2/3/4 times of the actual probability
since Pact is a small value). The results are shown in Table 5 (–means no results because the threshold is larger than 1.).
It can be observed that for benchmark systems, similarly or
identical models are learned by LAR for different r-values. The
reason is that for these relatively small systems, it is easy to learna model which produces accurate verification results after few
iterations. In contrast, for the SWaT system, LAR learns a coarser
model with fewer states, and less accurate result (which is stillgood enough to prove the property). We thus have the following
answer to RQ3.

56

7 8 9 10 11 12 13 14 15
Iterationnand-2nand-3nand-4swat-2swat-3Fig. 11: The time distribution of LAR in each iteration.

Answer to RQ3: LAR is able to learn models at different
abstraction levels in a property-guided way.

Threats to validity The above experiments successfully show theeffectiveness and efficiency of LAR over the test subjects. In thefollowing, we discuss several threats to the validity. First of all,it can be observed that a strict property (with probability close to
the actual probability) requires learning a detailed model, whereasa loose property requires a coarse model. In the worse case, if
the property can only be verified with all details in the system,
then we must refine all the way until every detail is included.
One question is then how we know whether the property is strict
or not so as to tell whether LAR will be effective. In general,
there is no good solution. Secondly, there is a tradeoff between thecomplexity of the classification algorithm to generate the predicate

13

and the interpretability of the learned model. For example, if thedataset is not linear separable and we apply kernel functions for
SVM, the generated predicate will not be easy to interpret. For
real-world complex systems, it might be possible that a linear
classifier does not exist, in which case we will either fail to learna model (without adopting kernels for SVM) or learn a modelthat is not intuitive for understanding (adopting kernels for SVM).
Thirdly, LAR refines the abstraction by choosing a particularspurious transition and separate the concrete states there. Thus,
the selection of different spurious transitions may lead to different
ways of refinement and thus models of different quality. Lastly,
LAR uses statistical hypothesis testing to check the spuriousnessof a counterexample in every iteration. An alternative way is to
apply SMC to check the given property directly, learn a modelfrom the traces captured during SMC if the property is violated
and explain to the user how the system fails. It is in general hardto predict which approach is more efficient because it depends
on the specific property and system. For instance, in case theproperty is indeed violated by the system, the alternative approach
might be more efficient in triggering such violations. However, theimprovement depends on the difference between the probability
threshold in the property and the actual probability of property
violation. The larger the difference, the more significant is the
improvement. In reality, CPS are usually equipped with safetymechanisms to avoid safety violations, which means that theprobability of the actual safety violation is usually low. In casethe property is satisfied, the comparison boils down to comparing
the efficiency of spuriousness checking and the efficiency of
SMC, which is also hard to tell. According to our experiments,
a spurious counterexample can usually be checked quickly using
SPRT during each iteration due to the wrong abstraction. On theother hand, SMC for a property with low probability may take along time. In the future, we will evaluate them in a separate work.

5

R ELATED W ORKThis work takes a further step towards the emerging trend toleverage system data for formal verification. It extends the recent
line of work to ‘learn’ (probabilistic especially) models (e.g., in
the form of DTMC, CTMC, stationary models and MDPs) fromsystem data for model checking [16], [40], [41], [42], [49] inorder to avoid manual modeling. Existing learning algorithms areoften based on algorithms designed for learning (probabilistic)
automata, as evidenced in [7], [13], [14], [21], [47], [48]. In [12],reinforcement learning algorithms are adopted to verify Markov
decision processes, without constructing explicit models. LAR
complements these model learning approaches with a CEGARstyle framework so that model learning can be done in a moreguided way, i.e., learn at the proper level of abstraction towards
the verification of certain properties. On the other hand, rather
than learning a single model from system data, the authors of [4],[24] proposes a Bayesian inference approach which performs
verification over the entire property- and model-based feasibleclass of models while providing a confidence over the datagenerating system.
This work is also closely related to the following line ofwork which aims to quantitatively verify stochastic hybrid systems
with confidence. In [5], [22], [25], [52], the authors uses formal
abstraction to quantitatively approximate the system with an
abstract computable model. The approximation is parameterized,
which then allows to quantify the distance between the models aswell as their solution processes [59]. Furthermore, a CEGARstyle procedure is proposed to refine the abstraction when theapproximate model is not satisfactory [53].
SMC [19], [46], [50], [56], [57] is another line of work forquantitative verification that can be applied when the systemmodel is not available. Hypothesis testing is initially adopted
by SMC mainly for bounded properties. There is some recent
work on extending SMC to unbounded properties [46], [56], andcombining learning and abstraction for faster SMC [43]. The maindifference between LAR and SMC is that LAR generates models
as a part of the verification results, which would offer knowledge
or insight on how the system works and why the property isverified. Furthermore, because LAR verifies the system based on
the learned model, it is not limited to bounded properties.
The main idea of this work is inspired by CEGAR [17], [18],[29], [30], [35] and in particular its extension to probabilistic
systems. The fundamental questions and pragmatic issues ofprobabilistic abstraction refinement are first explored in [31] in thecontext of predicate abstraction [23], [54], where a probabilistic
counterexample (obtained using the approach documented in [26])is analyzed to refine an abstraction. Compared to CEGAR andprobabilistic CEGAR, LAR is different as LAR does not require
any user-provided system models, which yields a completely
automatic verification framework from system data.

6

C ONCLUSION

In this work, we propose a framework to automatically verify
discrete-time complex systems without manual modeling througha combination of learning, abstraction and refinement. Our evaluation shows that LAR not only is more effective and efficientin verifying systems than state-of-the-art learning approaches byautomatically identifying a level of abstraction in a propertyguided way, but also generates models of high quality which could
be useful for subsequent system analysis purposes like runtime
monitoring or model-based testing. Our main contribution lies inproposing such an automatic verification framework from systemdata, a systematic way to analyze spurious counterexamples forrefinement, and adopt SVM to generate new predicates fromsystem data directly without the assumption of having the original
system model. In the future, we plan to compare our approachwith statistical model checking by conducting a more systematic
empirical study and extend the work to Markov Decision Process
to support modeling and verification of a richer range of systems.

R EFERENCES
[1]
[2]
[3]
[4]

[5]

[6]
[7]
[8]
[9]

https://github.com/wang-jingyi/Ziqian.
https://github.com/wang-jingyi/Ziqian evaluation.
https://itrust.sutd.edu.sg/research/testbeds/secure-water-treatment-swat/.
Alessandro Abate. Formal verification of complex systems: modelbased and data-driven methods. In Proceedings of the 15th ACM-IEEE
International Conference on Formal Methods and Models for System
Design, pages 91–93. ACM, 2017.
Alessandro Abate, Luboš Brim, Milan Češka, and Marta Kwiatkowska.
Adaptive aggregation of markov chains: Quantitative analysis of chemical reaction networks. In International Conference on Computer Aided
Verification, pages 195–213. Springer, 2015.
Thomas Abeel, Yves Van de Peer, and Yvan Saeys. Java-ml: A machinelearning library. The Journal of Machine Learning Research, 10:931–
934, 2009.
Dana Angluin. Learning regular sets from queries and counterexamples.
Information and computation, 75(2):87–106, 1987.
Dana Angluin. Identifying languages from stochastic examples. 1988.
A.Wald. Sequential Analysis. Wiley, 1947.

14[10] Christel Baier, Holger Hermanns, Joost-Pieter Katoen, and Verena Wolf.
Comparative branching-time semantics for markov chains. In International Conference on Concurrency Theory, pages 492–507. Springer,
2003.
[11] Christel Baier, Joost-Pieter Katoen, et al. Principles of model checking,volume 26202649. MIT press Cambridge, 2008.
[12] Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelı́k, Vojtěch Forejt,
Jan Křetı́nskỳ, Marta Kwiatkowska, David Parker, and Mateusz Ujma.
Verification of markov decision processes using learning algorithms.
In Automated Technology for Verification and Analysis, pages 98–114.
Springer, 2014.
[13] Rafael C Carrasco and José Oncina. Learning stochastic regular grammars by means of a state merging method. In Grammatical Inference
and Applications, pages 139–152. Springer, 1994.
[14] Rafael C Carrasco and Jose Oncina. Learning deterministic regular
grammars from stochastic samples in polynomial time. Informatiquethéorique et applications, 33(1):1–19, 1999.
[15] Chih-Chung Chang and Chih-Jen Lin. Libsvm: a library for support vector machines. ACM Transactions on Intelligent Systems and Technology(TIST), 2(3):27, 2011.
[16] Yingke Chen, Hua Mao, Manfred Jaeger, Thomas Dyhre Nielsen,
Kim Guldstrand Larsen, and Brian Nielsen. Learning markov models
for stationary system behaviors. In NASA Formal Methods, pages 216–
230. Springer, 2012.
[17] Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut
Veith. Counterexample-guided abstraction refinement. In International
Conference on Computer Aided Verification, pages 154–169. Springer,
2000.
[18] Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut
Veith. Counterexample-guided abstraction refinement for symbolicmodel checking. Journal of the ACM (JACM), 50(5):752–794, 2003.
[19] Edmund M Clarke and Paolo Zuliani. Statistical model checking forcyber-physical systems. In Automated Technology for Verification andAnalysis, pages 1–12. Springer, 2011.
[20] Corinna Cortes and Vladimir Vapnik. Support-vector networks. Machinelearning, 20(3):273–297, 1995.
[21] Colin De la Higuera. Grammatical inference, volume 96. Cambridge
University Press Cambridge, 2010.
[22] Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. Adaptive andsequential gridding procedures for the abstraction and verification ofstochastic processes. SIAM Journal on Applied Dynamical Systems,
12(2):921–956, 2013.
[23] Susanne Graf and Hassen Saı̈di. Construction of abstract state graphswith pvs. In Computer aided verification, pages 72–83. Springer, 1997.
[24] Sofie Haesaert, Paul MJ Van den Hof, and Alessandro Abate. Data-driven
and model-based verification via bayesian identification and reachability
analysis. Automatica, 79:115–126, 2017.
[25] Sofie Haesaert, Sadegh Esmaeil Zadeh Soudjani, and Alessandro Abate.
Verification of general markov decision processes by approximate similarity relations and policy refinement. SIAM Journal on Control andOptimization, 55(4):2333–2367, 2017.
[26] Tingting Han and Joost-Pieter Katoen. Counterexamples in probabilistic
model checking. Springer, 2007.
[27] Hans Hansson and Bengt Jonsson. A logic for reasoning about time andreliability. Formal aspects of computing, 6(5):512–535, 1994.
[28] Klaus Havelund and Grigore Roşu. Synthesizing monitors for safety
properties. In Tools and Algorithms for the Construction and Analysis of
Systems, pages 342–356. Springer, 2002.
[29] Thomas A Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L
McMillan. Abstractions from proofs. In ACM SIGPLAN Notices,volume 39, pages 232–244. ACM, 2004.
[30] Thomas A Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire
Sutre. Lazy abstraction. ACM SIGPLAN Notices, 37(1):58–70, 2002.
[31] Holger Hermanns, Björn Wachter, and Lijun Zhang. Probabilistic cegar.
In Computer Aided Verification, pages 162–175. Springer, 2008.
[32] Cyrille Jegourel, Sun Jun, and Jin-Song Dong. Sequential Schemes forFrequentist Estimation of Properties in Statistical Model Checking. In
QEST, 2017.
[33] Gabor Karsai and Janos Sztipanovits. Model-integrated developmentof cyber-physical systems. In IFIP International Workshop on Software Technolgies for Embedded and Ubiquitous Systems, pages 46–54.
Springer, 2008.
[34] Christopher Kermorvant and Pierre Dupont. Stochastic grammaticalinference with multinomial tests. In Grammatical Inference: Algorithms
and Applications, pages 149–160. Springer, 2002.

[35] Daniel Kroening, Alex Groce, and Edmund Clarke. Counterexample
guided abstraction refinement via program execution. In Formal Methods
and Software Engineering, pages 224–238. Springer, 2004.
[36] M. Kwiatkowska, G. Norman, and D. Parker. The PRISM benchmark
suite. In Proc. 9th International Conference on Quantitative Evaluationof SysTems (QEST’12), pages 203–204. IEEE CS Press, 2012.
[37] Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM DTMC
benchmark models. http://www.prismmodelchecker.org/benchmarks/.
[38] Marta Kwiatkowska, Gethin Norman, and David Parker. Prism 4.0: Verification of probabilistic real-time systems. In International Conference
on Computer Aided Verification, pages 585–591. Springer, 2011.
[39] Axel Legay, Benoı̂t Delahaye, and Saddek Bensalem. Statistical model
checking: An overview. In International Conference on Runtime Verification, pages 122–135. Springer, 2010.
[40] Hua Mao, Yingke Chen, Manfred Jaeger, Thomas D Nielsen, Kim G
Larsen, and Brian Nielsen. Learning probabilistic automata for model
checking. In Quantitative Evaluation of Systems (QEST), 2011 EighthInternational Conference on, pages 111–120. IEEE, 2011.
[41] Hua Mao, Yingke Chen, Manfred Jaeger, Thomas D Nielsen, Kim G
Larsen, and Brian Nielsen. Learning markov decision processes formodel checking. arXiv preprint arXiv:1212.3873, 2012.
[42] Hua Mao, Yingke Chen, Manfred Jaeger, Thomas D. Nielsen, Kim G.
Larsen, and Brian Nielsen. Learning deterministic probabilistic automata
from a model checking perspective. Machine Learning, 105(2):255–299,
Nov 2016.
[43] Ayoub Nouri, Balaji Raman, Marius Bozga, Axel Legay, and Saddek
Bensalem. Faster statistical model checking by means of abstraction
and learning. In International Conference on Runtime Verification, pages
340–355. Springer, 2014.
[44] Alexander Pretschner. Model-based testing. In Software Engineering,
2005. ICSE 2005. Proceedings. 27th International Conference on, pages
722–723. IEEE, 2005.
[45] M. Reiter and A. Rubin. Crowds: Anonymity for web transactions. ACM
Transactions on Information and System Security (TISSEC, 1(1):66–92,
1998.
[46] Christian Rohr. Simulative model checking of steady state and timeunbounded temporal operators. In Transactions on Petri Nets and Other
Models of Concurrency VIII, pages 142–158. Springer, 2013.
[47] Dana Ron, Yoram Singer, and Naftali Tishby. On the learnability andusage of acyclic probabilistic finite automata. In Proceedings of theeighth annual conference on Computational learning theory, pages 31–
40. ACM, 1995.
[48] Dana Ron, Yoram Singer, and Naftali Tishby. The power of amnesia:
Learning probabilistic automata with variable memory length. Machinelearning, 25(2-3):117–149, 1996.
[49] Koushik Sen, Mahesh Viswanathan, and Gul Agha. Learning continuous
time markov chains from sample executions. In Quantitative Evaluationof Systems, 2004. QEST 2004. Proceedings. First International Conference on the, pages 146–155. IEEE, 2004.
[50] Koushik Sen, Mahesh Viswanathan, and Gul Agha. Statistical model
checking of black-box probabilistic systems. In Computer Aided Verification, pages 202–215. Springer, 2004.
[51] A Prasad Sistla, Miloš Žefran, and Yao Feng. Runtime monitoring of
stochastic cyber-physical systems with hybrid state. In International
Conference on Runtime Verification, pages 276–293. Springer, 2011.
[52] Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. Quantitative
approximation of the probability distribution of a markov process byformal abstractions. arXiv preprint arXiv:1504.00039, 2015.
[53] Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, and Alessandro
Abate. Quantitative model-checking of controlled discrete-time markov
processes. Information and Computation, 253:1–35, 2017.
[54] Bjorn Wachter, Lijun Zhang, and Holger Hermanns. Probabilistic model
checking modulo theories. In Fourth International Conference on the
Quantitative Evaluation of Systems., pages 129–140. IEEE, 2007.
[55] Jingyi Wang, Jun Sun, Qixia Yuan, and Jun Pang. Should we learn
probabilistic models for model checking? a new approach and an empirical study. In International Conference on Fundamental Approaches to
Software Engineering, pages 3–21. Springer, 2017.
[56] Håkan LS Younes, Edmund M Clarke, and Paolo Zuliani. Statisticalverification of probabilistic properties with unbounded until. In Formal
Methods: Foundations and Applications, pages 144–160. Springer, 2011.
[57] Håkan LS Younes and Reid G Simmons. Probabilistic verification of
discrete event systems using acceptance sampling. In Computer Aided
Verification, pages 223–235. Springer, 2002.
[58] H.L.S Younes. Verification and Planning for Stochastic Processes with
Asynchronous Events. PhD thesis, Carnegie Mellon, 2005.

15[59] Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, and John Lygeros. Symbolic control of stochastic systems
via approximately bisimilar finite abstractions. IEEE Transactions on
Automatic Control, 59(12):3135–3150, 2014.

A PPENDIX A
B OUND ON THE LEARNING ERROR
Let A = (aij )1≤i,j≤m be a stochastic matrix of size m × m,
which represents the actual transition matrix of M and Â =(âij )1≤i,j≤m be that of DP . For simplicity, we assume Â islearned through a simple algorithm based on Monte Carlo frequency estimate. That is, âij = nij /ni where ni is the number oftimes a transition has been taken from state i and nij the numberof times that transition from state i to state j has been taken. We
denote n0 = min1≤i≤m ni .
Given a precision bound  and a confidence bound δ , we showthat it is feasible to determine a sampling scheme that guarantees
after a minimal number of samples:

P (||Â − A|| > ) < δ(4)where ||Â − A|| denotes a matrix distance between Â and A.
In what follows, let the distance be defined as ||Â − A|| =supij |âij − aij |.

P (||Â − A|| > )

= P (sup |âij − aij | > )ij[
= P  {|âij − aij | > } 
ij

≤

X

P (|âij − aij | > )

ij

≤

X

≤

X

ij

P (|

nij
− aij | > )ni

Jingyi Wang is currently a research fellow inthe pillar of Information Systems Technology and
Design at Singapore University of Technology
and Design, Singapore, where he obtained his
PhD in March 2018. Before this, he got his Bachelor of Engineering degree in Information Engineering from Xi’an Jiaotong University, Xi’an,
China in 2013. His main research interests are
to apply machine learning and statistical techniques into formal verification as well as security
problems in deep learning systems.

Jun Sun is currently an associate professor at
Singapore University of Technology and Design(SUTD). He received Bachelor and PhD degrees
in computing science from National University ofSingapore (NUS) in 2002 and 2006. In 2007,
he received the prestigious LEE KUAN YEW
postdoctoral fellowship. He has been a faculty
member of SUTD since 2010. He was a visiting
scholar at MIT from 2011-2012. Jun’s researchinterests include software engineering, formal
methods, program analysis and cyber-security.
He is the co-founder of the PAT model checker.

Shengchao Qin got his PhD in Applied Mathematics from Peking University and also worked
as a Postdoctoral Research Fellow in National
University of Singapore under the SingaporeMIT Alliance program, before moving his job to
UK. His research interests lie mainly in formal
methods, software engineering and programming languages, in particular, formal specification and modelling, program analysis and verification, theories of programming, program logic
such as separation logic. To this date he has
published over 90 papers in international journals and peer-refereed
international conferences.

2 exp(−2ni 2 ) (Okamoto bound)ij≤ 2m2 exp(−2n0 2 )Based on the above, given δ and , Π must contain enoughδ
traces such that each state is visited at least n0 = d 212 log 2m2 e
if we are to guarantee that the learned model satisfies the constraint
stated in Equation 4.
This bound is conservative. However, this sampling scheme
terminates with probability 1 since all the states are reachable.
Furthermore, there are several ways to improve this bound. First,
the term m2 could be replaced by the number of transitions K
such that aij is different from 0 or 1. In that case, P (|âij −aij | > ) is necessarily equal to 0, then sequential frequentist
methods based on sharper bounds may be used (e.g. [32]) insteadof the used Okamoto bound. Besides, the number of samples isalso impacted by the choice of . Finally, the choice of the matrix
distance is also important. For example, at the learning level, we
could prefer a distance that takes into account probabilities pi ofbeing in state i in order to guarantee a fine per-transition error
bound over states that are often visited and a coarser bound overstates that are not often visited. This is left to future work.

Cyrille Jegourel was born in France, on October 22, 1984. He received the B.S. degree inmathematics in 2005, the M.S. degree in statistical engineering in 2008, and the Ph.D. degree incomputer science in 2014 from the University ofRennes 1, France. He was a development andresearch engineer at Inria Rennes, Bretagne
Atlantique, France, from time to time between
2008 and 2015. He was a postdoctoral Research
Fellow at the National University of Singapore,
Singapore, in 2015. In 2016, he joined the Singapore University of Technology and Design, Singapore, where he wasengaged as a Research Fellow to work on sampling techniques andstatistical aspects for formal methods.