On-the-fly Probabilistic Model Checking
Diego Latella (ISTI - CNR), Michele Loreti (Universit\`a di Firenze),, Mieke Massink (ISTI - CNR)

TL;DR
This paper introduces an efficient on-the-fly probabilistic model checking method for PCTL, suitable for systems with many components, focusing on local state space exploration to improve efficiency.
Contribution
It presents a novel on-the-fly PCTL model checking approach that is parametric and includes both bounded and unbounded modalities, with proven correctness and efficiency comparisons.
Findings
Outperforms global model checkers on representative applications
Handles both bounded and unbounded until modalities effectively
Suitable for systems with many parallel components
Abstract
Model checking approaches can be divided into two broad categories: global approaches that determine the set of all states in a model M that satisfy a temporal logic formula f, and local approaches in which, given a state s in M, the procedure determines whether s satisfies f. When s is a term of a process language, the model checking procedure can be executed "on-the-fly", driven by the syntactical structure of s. For certain classes of systems, e.g. those composed of many parallel components, the local approach is preferable because, depending on the specific property, it may be sufficient to generate and inspect only a relatively small part of the state space. We propose an efficient, on-the-fly, PCTL model checking procedure that is parametric with respect to the semantic interpretation of the language. The procedure comprises both bounded and unbounded until modalities. The…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Semantic Web and Ontologies · Natural Language Processing Techniques
