An Enhanced Interface-Based Probabilistic Compositional Verification Approach

In this paper, we aim to advance the state of the art in the verification process of systems, predominantly modeled as Probabilistic Automata (PA). This model accommodates both nondeterministic and probabilistic behaviors. Our primary strategy to address the notorious state space explosion problem inherent in model checking is the adoption of abstraction and compositional verification techniques, culminating in the development of a distributed verification approach centered on the communication interface amongst composed automata. Initially, the abstraction technique refines the system in relation to the requirement under verification and amalgamates states demonstrating comparable behaviors. Not only does it simplify the system, but it also enables a decomposition of global requirements into local ones. This decomposition process facilitates parallel verification and securely allows inference on the global requirement from local results. Moreover, the soundness of our proposed framework has been substantiated, ensuring that it correctly interprets and applies the properties of the system under scrutiny. In the final phase, we leveraged the PRISM model checker to assess the effectiveness of our proposed framework. This evaluation was carried out on three benchmark tests, providing empirical evidence to support the benefits of our approach. Our contribution to the field lies in the novel combination of abstraction and compositional verification techniques in a distributed verification framework, validated through theoretical soundness proofs and practical tests using the PRISM model checker. This result paves the way for more efficient and scalable model-checking processes for Probabilistic Automata.