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

Radu Mateescu 1 José Requeno 1, 2
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 (Prob-abilistic Transition Systems) labeled by actions containing data values and probabilities. We propose a new regular probabilistic operator that specifies the probability measure of a path described 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.
Type de document :
Article dans une revue
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2018, 20 (5), pp.563-587. 〈10.1007/s10009-018-0499-0〉
Liste complète des métadonnées

Littérature citée [40 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01862754
Contributeur : Radu Mateescu <>
Soumis le : lundi 27 août 2018 - 16:44:46
Dernière modification le : samedi 15 décembre 2018 - 01:50:10
Document(s) archivé(s) le : mercredi 28 novembre 2018 - 15:38:04

Fichier

mateescu_requeno_prob.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Radu Mateescu, José Requeno. On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2018, 20 (5), pp.563-587. 〈10.1007/s10009-018-0499-0〉. 〈hal-01862754〉

Partager

Métriques

Consultations de la notice

71

Téléchargements de fichiers

35