Assume-Guarantee Abstraction Refinement for Probabilistic Systems

TL;DR

This paper introduces an automated assume-guarantee abstraction refinement method for probabilistic systems, enabling efficient strong simulation checking between system components and specifications.

Contribution

It presents a novel approach to counterexample characterization and an abstraction refinement algorithm for probabilistic systems, with implementation and promising results.

Findings

Effective counterexample generation for probabilistic systems

Automated abstraction refinement improves simulation checking

Encouraging experimental results on benchmark cases

Abstract

We describe an automated technique for assume-guarantee style checking of strong simulation between a system and a specification, both expressed as non-deterministic Labeled Probabilistic Transition Systems (LPTSes). We first characterize counterexamples to strong simulation as "stochastic" trees and show that simpler structures are insufficient. Then, we use these trees in an abstraction refinement algorithm that computes the assumptions for assume-guarantee reasoning as conservative LPTS abstractions of some of the system components. The abstractions are automatically refined based on tree counterexamples obtained from failed simulation checks with the remaining components. We have implemented the algorithms for counterexample generation and assume-guarantee abstraction refinement and report encouraging results.