000079737 001__ 79737
000079737 005__ 20200117221611.0
000079737 0247_ $$2doi$$a10.1007/s10009-018-0499-0
000079737 0248_ $$2sideral$$a107689
000079737 037__ $$aART-2018-107689
000079737 041__ $$aeng
000079737 100__ $$aMateescu, R.
000079737 245__ $$aOn-the-fly model checking for extended action-based probabilistic operators
000079737 260__ $$c2018
000079737 5060_ $$aAccess copy available to the general public$$fUnrestricted
000079737 5203_ $$aThe 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.
000079737 536__ $$9info:eu-repo/grantAgreement/EC/FP7/318490/EU/Self Energy-Supporting Autonomous Computation/SENSATION
000079737 540__ $$9info:eu-repo/semantics/openAccess$$aAll rights reserved$$uhttp://www.europeana.eu/rights/rr-f/
000079737 590__ $$a1.27$$b2018
000079737 591__ $$aCOMPUTER SCIENCE, SOFTWARE ENGINEERING$$b66 / 107 = 0.617$$c2018$$dQ3$$eT2
000079737 592__ $$a0.472$$b2018
000079737 593__ $$aSoftware$$c2018$$dQ2
000079737 593__ $$aInformation Systems$$c2018$$dQ2
000079737 655_4 $$ainfo:eu-repo/semantics/article$$vinfo:eu-repo/semantics/acceptedVersion
000079737 700__ $$0(orcid)0000-0001-5111-8357$$aRequeno, J.I.$$uUniversidad de Zaragoza
000079737 7102_ $$15007$$2570$$aUniversidad de Zaragoza$$bDpto. Informát.Ingenie.Sistms.$$cÁrea Lenguajes y Sistemas Inf.
000079737 773__ $$g20, 5 (2018), 563-587$$pInt. j. softw. tools technol. transf.$$tInternational journal on software tools for technology transfer$$x1433-2779
000079737 8564_ $$s857726$$uhttps://zaguan.unizar.es/record/79737/files/texto_completo.pdf$$yPostprint
000079737 8564_ $$s108433$$uhttps://zaguan.unizar.es/record/79737/files/texto_completo.jpg?subformat=icon$$xicon$$yPostprint
000079737 909CO $$ooai:zaguan.unizar.es:79737$$particulos$$pdriver
000079737 951__ $$a2020-01-17-21:48:42
000079737 980__ $$aARTICLE