Sciweavers

POPL
2015
ACM

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems

8 years 6 months ago
Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems
We propose the first sound and complete learning-based compositional verification technique for probabilistic safety properties on concurrent systems where each component is an Markov decision process. Different from previous works, weighted assumptions are introduced to attain completeness of our framework. Since weighted assumptions can be implicitly represented by multi-terminal binary decision diagrams (MTBDD’s), we give an L∗ -based learning algorithm for MTBDD’s to infer weighted assumptions. Experimental results suggest promising outlooks for our compositional technique. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Model Checking General Terms Theory, Verification Keywords Compositional verification, probabilistic model checking, algorithmic learning
Fei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where POPL
Authors Fei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang
Comments (0)