On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators

Radu Mateescu 1 José Ignacio Requeno 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The quantitative analysis of concurrent systems requires expressive and user-friendly property languages combining temporal, data-handling, and quantitative aspects. In this paper, we aim at facilitating the quantitative analysis of systems modeled as PTSs (Probabilistic Transition Systems) labeled by actions containing data values and probabilities. We propose a new regular probabilistic operator that computes the probability measure of a path specified by a generalized regular formula involving arbitrary computations on data values. This operator, which subsumes the Until operators of PCTL and their action-based counterparts, can provide useful quantitative information about paths having certain (e.g., peak) cost values. We integrated the regular probabilistic operator into MCL (Model Checking Language) and we devised an associated on-the-fly model checking method, based on a combined local resolution of linear and Boolean equation systems. We implemented the method in the EVALUATOR model checker of the CADP toolbox and experimented it on realistic PTSs modeling concurrent systems.
Document type :
Conference papers
Springer Verlag. 23rd International SPIN symposium on Model Checking of Software, Apr 2016, Eindhoven, Netherlands. 2016, SPIN'2016. 〈http://www.spin2016.info/〉. 〈10.1007/978-3-319-32582-8_13〉
Liste complète des métadonnées

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01280129
Contributor : Radu Mateescu <>
Submitted on : Monday, May 9, 2016 - 3:49:15 PM
Last modification on : Thursday, May 12, 2016 - 9:42:46 AM
Document(s) archivé(s) le : Wednesday, May 25, 2016 - 8:12:01 AM

File

Mateescu-Requeno-16.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Radu Mateescu, José Ignacio Requeno. On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators. Springer Verlag. 23rd International SPIN symposium on Model Checking of Software, Apr 2016, Eindhoven, Netherlands. 2016, SPIN'2016. 〈http://www.spin2016.info/〉. 〈10.1007/978-3-319-32582-8_13〉. 〈hal-01280129〉

Share

Metrics

Record views

325

Files downloads

73