Skip to main content

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.

Speaker bio

Anvesh Komuravelli is a PhD student in the Computer Science Department at Carnegie Mellon University (CMU), Pittsburgh, working with Prof. Edmund M. Clarke. He earned his B.Tech (Hons.) degree in Computer Science and Engineering from the Indian Institute of Technology (IIT) Kharagpur in 2009 when he was awarded with the President of India Gold Medal. He began his research in Computer Science in late 2007 by working on some problems in Computational Geometry, at IIT and at ETH, Switzerland. In 2008, he started working on automatically verifying mixed-signal circuits at IIT and got interested in the field of Formal Verification. He wrote a senior thesis on backward reasoning of Linear Temporal properties to analyze potentially deep bugs in 2009. At CMU, he continues to work on developing algorithms and techniques for scaling Model Checking to complex systems, both probabilistic and non-probabilistic. Besides academics, he is an amateur vocalist and is very passionate about music in general.

Share this: