On-the-fly model checking for extended action-based probabilistic operators
Financiación FP7 / Fp7 Funds
Resumen: 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 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.
Idioma: Inglés
DOI: 10.1007/s10009-018-0499-0
Año: 2018
Publicado en: International journal on software tools for technology transfer 20, 5 (2018), 563-587
ISSN: 1433-2779

Factor impacto JCR: 1.27 (2018)
Categ. JCR: COMPUTER SCIENCE, SOFTWARE ENGINEERING rank: 66 / 107 = 0.617 (2018) - Q3 - T2
Factor impacto SCIMAGO: 0.472 - Software (Q2) - Information Systems (Q2)

Financiación: info:eu-repo/grantAgreement/EC/FP7/318490/EU/Self Energy-Supporting Autonomous Computation/SENSATION
Tipo y forma: Artículo (PostPrint)
Área (Departamento): Área Lenguajes y Sistemas Inf. (Dpto. Informát.Ingenie.Sistms.)

Derechos Reservados Derechos reservados por el editor de la revista

Exportado de SIDERAL (2020-01-17-21:48:42)

Este artículo se encuentra en las siguientes colecciones:

 Registro creado el 2019-08-19, última modificación el 2020-01-17

Valore este documento:

Rate this document:
(Sin ninguna reseña)