79737 20200117221611.0 doi 10.1007/s10009-018-0499-0 sideral 107689 ART-2018-107689 eng Mateescu, R. On-the-fly model checking for extended action-based probabilistic operators 2018 Access copy available to the general public Unrestricted 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. info:eu-repo/grantAgreement/EC/FP7/318490/EU/Self Energy-Supporting Autonomous Computation/SENSATION info:eu-repo/semantics/openAccess All rights reserved http://www.europeana.eu/rights/rr-f/ 1.27 2018 COMPUTER SCIENCE, SOFTWARE ENGINEERING 66 / 107 = 0.617 2018 Q3 T2 0.472 2018 Software 2018 Q2 Information Systems 2018 Q2 info:eu-repo/semantics/article info:eu-repo/semantics/acceptedVersion (orcid)0000-0001-5111-8357 Requeno, J.I. Universidad de Zaragoza 5007 570 Universidad de Zaragoza Dpto. Informát.Ingenie.Sistms. Área Lenguajes y Sistemas Inf. 20, 5 (2018), 563-587 Int. j. softw. tools technol. transf. International journal on software tools for technology transfer 1433-2779 857726 http://zaguan.unizar.es/record/79737/files/texto_completo.pdf Postprint 108433 http://zaguan.unizar.es/record/79737/files/texto_completo.jpg?subformat=icon icon Postprint oai:zaguan.unizar.es:79737 articulos driver 2020-01-17-21:48:42 ARTICLE