REVIEW 1 cited by
Assume-Guarantee Abstraction Refinement for Probabilistic Systems
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original 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.
Forward citations
Cited by 1 Pith paper
-
Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy
A pipeline that turns collected runs of a vision-based controller into an interval MDP, verifies a safety lower bound, and reuses Bayesian conformance to extend the bound to new environments.
Discussion (0). Continue with ORCID to comment.