Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(10)
Automatic Generation
Case Study
Compositional Verification
Finite Automata
Lower and Upper Bound
Probabilistic Automata
Probabilistic Model
Probabilistic Model Checking
Probabilistic System
Safety Properties
Subscribe
Academic
Publications
Compositional Verification of Probabilistic Systems Using Learning
Compositional Verification of Probabilistic Systems Using Learning,10.1109/QEST.2010.24,Lu Feng,Marta Z. Kwiatkowska,David Parker
Edit
Compositional Verification of Probabilistic Systems Using Learning
(
Citations: 5
)
BibTex

RIS

RefWorks
Download
Lu Feng
,
Marta Z. Kwiatkowska
,
David Parker
We present a fully automated technique for
compositional verification
of probabilistic systems. Our approach builds upon a recently proposed assumeguarantee framework for probabilistic automata, in which assumptions and guarantees are probabilistic safety properties, represented using finite automata. A limitation of this work is that the assumptions need to be created manually. To overcome this, we propose a novel learning technique based on the L* algorithm, which automatically generates probabilistic assumptions using the results of queries executed by a
probabilistic model
checker. Learnt assumptions either establish satisfaction of the verification problem or are used to generate a probabilistic counterexample that refutes it. In the case where an assumption cannot be generated, lower and upper bounds on the probability of satisfaction are produced. We illustrate the applicability of the approach on a range of case studies.
Conference:
Quantitative Evaluation of Systems  QEST
, pp. 133142, 2010
DOI:
10.1109/QEST.2010.24
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
dx.doi.org
)
(
www.informatik.unitrier.de
)
(
ieeexplore.ieee.org
)
(
ieeexplore.ieee.org
)
More »
Citation Context
(5)
...Possible directions for future work include extending our compositional verification approach with learningbased assumption generation, as [
17
] does for the simpler framework of [21], and investigation of continuoustime models...
Vojtech Forejt
,
et al.
Quantitative Multiobjective Verification for Probabilistic Systems
...In recent work [
20
], we showed how learning could also be successfully used to generate the probabilistic assumptions needed for the compositional verification of probabilistic systems...
...This approach was proposed in [
20
] and shown to be applicable on several large case studies...
...In this section, we give a highlevel overview of the approach and describe the key underlying ideas; for the technical details, the reader is referred to [
20
]...
...upper bound can also be generated (see [
20
] for details)...
...Fig. 3. Overview of probabilistic assumption generation [
20
], using an adaption of L*: generates assumption � A� pA for verification of M1 � M2 = � G� pG using rule (ASym)...
...Firstly, a counterexample may constitute multiple traces; this is because the results of the model checking queries executed by the teacher yield probabilistic counterexamples [24], which comprise multiple paths (again, see [
20
] for precise details)...
...The approach outlined in the previous section was successfully used in [
20
] to automatically generate probabilistic assumptions for several large case studies...
...We added NL* to our existing implementation from [
20
], which is based on an extension of PRISM [26] and the libalf [6] learning library...
...The first four are taken from [
20
]: clientserver benchmark models from [32] incorporating failures in one or all clients (clientserver1 and clientserverN ), Aspnes & Herlihy’s randomised consensus algorithm (consensus )a nd as ensor network exhibiting message losses (sensor network ). The fifth example is the MER model from above (mer ). Experiments were run on a 1.86GHz PC with 2GB RAM and we imposed a timeout of 24 hours...
Lu Feng
,
et al.
Automated Learning of Probabilistic Assumptions for Compositional Reas...
...In subsequent work [
33
], the process of generating an appropriate assumption hAi pA is also automated, using algorithmic learning techniques based on the L* algorithm...
Marta Kwiatkowska
,
et al.
Advances and challenges of probabilistic model checking
...In particular, we would like to exploit the assumeguarantee reasoning method [15,
9
] implemented in PRISM to analyse large models...
Felicita Di Giandomenico
,
et al.
Dependability Analysis and Verification for Connected Systems
...Other promising directions include: partial order reduction [49,31], symmetry reduction [66,39], algorithms for simulation and bisimulation relations [25,86] and compositional probabilistic verification techniques [69,
43
,38]...
Vojtěch Forejt
,
et al.
Automated Verification Techniques for Probabilistic Systems
References
(16)
Observing Branching Structure through Probabilistic Contexts
(
Citations: 18
)
Nancy A. Lynch
,
Roberto Segala
,
Frits W. Vaandrager
Journal:
Siam Journal on Computing  SIAMCOMP
, vol. 37, no. 4, pp. 9771013, 2007
Switched PIOA: Parallel composition via distributed scheduling
(
Citations: 13
)
Ling Cheung
,
Nancy A. Lynch
,
Roberto Segala
,
Frits W. Vaandrager
Journal:
Theoretical Computer Science  TCS
, vol. 365, no. 12, pp. 83108, 2006
Compositional Methods for Probabilistic Systems
(
Citations: 44
)
Luca De Alfaro
,
Thomas A. Henzinger
,
Ranjit Jhala
Conference:
International Conference on Concurrency Theory  CONCUR
, pp. 351365, 2001
AssumeGuarantee Verification for Probabilistic Systems
(
Citations: 12
)
Marta Z. Kwiatkowska
,
Gethin Norman
,
David Parker
,
Hongyang Qu
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 2337, 2010
Learning Regular Sets from Queries and Counterexamples
(
Citations: 657
)
Dana Angluin
Journal:
Information and Computation/information and Control  IANDC
, vol. 75, no. 2, pp. 87106, 1987
Sort by:
Citations
(5)
Quantitative Multiobjective Verification for Probabilistic Systems
(
Citations: 5
)
Vojtech Forejt
,
Marta Z. Kwiatkowska
,
Gethin Norman
,
David Parker
,
Hongyang Qu
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 112127, 2011
Automated Learning of Probabilistic Assumptions for Compositional Reasoning
Lu Feng
,
Marta Z. Kwiatkowska
,
David Parker
Conference:
Fundamental Approaches to Software Engineering  FASE
, pp. 217, 2011
Advances and challenges of probabilistic model checking
(
Citations: 2
)
Marta Kwiatkowska
,
Gethin Norman
,
David Parker
Conference:
Annual Allerton Conference on Communication, Control, and Computing  Allerton
, 2010
Dependability Analysis and Verification for Connected Systems
(
Citations: 2
)
Felicita Di Giandomenico
,
Marco Martinucci
,
Paolo Masci
,
Hongyang Qu
Conference:
Leveraging Applications of Formal Methods  ISOLA
, pp. 263277, 2010
Automated Verification Techniques for Probabilistic Systems
Vojtěch Forejt
,
Marta Kwiatkowska
,
Gethin Norman
,
David Parker