Quantitative Verification of Stochastic Regular Expressions

dc.contributor.authorYaman, Sinem Getir
dc.contributor.authorPavese, Esteban
dc.contributor.authorGrunske, Lars
dc.date.accessioned2021-05-03T20:33:20Z
dc.date.available2021-05-03T20:33:20Z
dc.date.issued2021
dc.departmentEge Üniversitesien_US
dc.description.abstractIn this article, we introduce a probabilistic verification algorithm for stochastic regular expressions over a probabilistic extension of the Action based Computation Tree Logic (ACTL*). The main results include a novel model checking algorithm and a semantics on the probabilistic action logic for stochastic regular expressions (SREs). Specific to our model checking algorithm is that SREs are defined via local probabilistic functions. Such functions are beneficial since they enable to verify properties locally for sub-components. This ability provides a flexibility to reuse the local results for the global verification of the system; hence, the framework can be used for iterative verification. We demonstrate how to model a system with an SRE and how to verify it with the probabilistic action based logic and present a preliminary performance evaluation with respect to the execution time of the reachability algorithm.en_US
dc.identifier.doi10.3233/FI-2021-2018
dc.identifier.endpage163en_US
dc.identifier.issn0169-2968
dc.identifier.issn1875-8681
dc.identifier.issn0169-2968en_US
dc.identifier.issn1875-8681en_US
dc.identifier.issue2en_US
dc.identifier.scopus2-s2.0-85102563966en_US
dc.identifier.scopusqualityQ3en_US
dc.identifier.startpage135en_US
dc.identifier.urihttps://doi.org10.3233/FI-2021-2018
dc.identifier.urihttps://hdl.handle.net/11454/69979
dc.identifier.volume179en_US
dc.identifier.wosWOS:000629178200004en_US
dc.identifier.wosqualityQ3en_US
dc.indekslendigikaynakWeb of Scienceen_US
dc.indekslendigikaynakScopusen_US
dc.language.isoenen_US
dc.publisherIos Pressen_US
dc.relation.ispartofFundamenta Informaticaeen_US
dc.relation.publicationcategoryMakale - Uluslararası Hakemli Dergi - Kurum Öğretim Elemanıen_US
dc.rightsinfo:eu-repo/semantics/closedAccessen_US
dc.subjectquantitative verificationen_US
dc.subjectprobabilistic verificationen_US
dc.subjectformal modelsen_US
dc.subjectstochastic regular expressionsen_US
dc.subjectprobabilistic regular expressionsen_US
dc.subjectstochastic algebraen_US
dc.subjectaction based logicen_US
dc.titleQuantitative Verification of Stochastic Regular Expressionsen_US
dc.typeArticleen_US

Dosyalar