Assume-Guarantee Reasoning of Simulation Conformance between Probabilistic Systems

Anvesh Komuravelli ( CMU )

Assume-Guarantee reasoning is a compositional technique for scalable verification of concurrent systems. In this talk, we discuss some new advancements in automating such reasoning applied to {\em probabilistic} systems. In particular, we address the problem of checking strong simulation conformance between a concurrent probabilistic system and a specification, also expressed as a probabilistic system. We discuss two alternative solutions to the problem. The first solution is based on the well-known counterexample-guided abstraction refinement loop where abstractions of components are used as assumptions and are iteratively refined in an assume-guarantee style. We also discuss an implementation of this solution which achieved encouraging results on a set of PRISM benchmarks. The second solution is based on machine learning algorithms to build the assumptions. As the counterexamples to strong simulation turn out to be trees, we discuss some new algorithms and decidability results for learning probabilistic systems from tree samples which can be then be applied to assume-guarantee reasoning. Finally, we try to relate these two solutions to the recent work done at Oxford on assume-guarantee reasoning for probabilistic safety properties. This is joint work with Corina S. Pasareanu and Edmund M. Clarke.