|
[FHKP11]
Lu Feng, Tingting Han, Marta Kwiatkowska and David Parker.
Learning-based Compositional Verification for Synchronous Probabilistic Systems.
In Proc. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), volume 6996 of LNCS, pages 511-521, Springer.
October 2011.
[pdf]
[bib]
[Presents a learning-based compositional verification framework which uses PRISM for executing individual queries.]
|
|
Downloads:
 pdf (402 KB)
 bib
|
|
Notes:
An extended version of this paper can be found in [FHKP11b].
The original publication is available at link.springer.com.
|
|
Links:
[Google]
[Google Scholar]
|
|
Abstract.
We present novel techniques for automated compositional verification of synchronous probabilistic systems.
First, we give an assume-guarantee framework for
verifying probabilistic safety properties of
systems modelled as discrete-time Markov chains.
Assumptions about system components are represented as probabilistic finite automata (PFAs)
and the relationship between components and assumptions is captured by weak language inclusion.
In order to implement this framework,
we develop a semi-algorithm to check language inclusion for PFAs
and a new active learning method for PFAs.
The latter is then used to automatically generate assumptions for compositional verification.
|