MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata

Autor: Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 154, Iss Proc. QAPL 2014, Pp 48-63 (2014)

Markov automata combine continuous time, probabilistic transitions, and nondeterminism in a single model. They represent an important and powerful way to model a wide range of complex real-life systems. However, such models tend to be large and diffi

Externí odkaz: https://doaj.org/article/db2b6edb92b54e81bce962ecaa994f47

Deciding probabilistic automata weak bisimulation: theory and practice

Autor: Andrea Turrini, Holger Hermanns, Vahid Hashemi, Luis María Ferrer Fioriti

Publikováno v: Formal Aspects of Computing. 28:109-143

Weak probabilistic bisimulation on probabilistic automata can be decided by an algorithm that needs to check a polynomial number of linear programming problems encoding weak transitions. It is hence of polynomial complexity. This paper discusses the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::a38da6f50c73ce0ed1cf09d1aa8bf019
https://doi.org/10.1007/s00165-016-0356-4

Synthesizing Probabilistic Invariants via Doob's Decomposition

Autor: Luis María Ferrer Fioriti, Justin Hsu, Gilles Barthe, Thomas Espitau

Publikováno v: Computer Aided Verification 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings
28th International Conference on Computer Aided Verification
28th International Conference on Computer Aided Verification, Jul 2016, Toronto, Canada. pp.43-61, ⟨10.1007/978-3-319-41528-4_3⟩
Computer Aided Verification ISBN: 9783319415277
CAV (1)

International audience; When analyzing probabilistic computations, a powerful approach is to first find a martingale—an expression on the program variables whose expectation remains invariant—and then apply the optional stopping theorem in order

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::baa14d645b6570d19a38e3d674542963
https://hal.science/hal-01561429

Probabilistic Termination

Autor: Luis María Ferrer Fioriti, Holger Hermanns

Publikováno v: POPL

We propose a framework to prove almost sure termination for probabilistic programs with real valued variables. It is based on ranking supermartingales, a notion analogous to ranking functions on non-probabilistic programs. The framework is proven sou

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::971518c64c0f53f9c9154f8e35fee64c
https://doi.org/10.1145/2676726.2677001

Cost vs. Time in Stochastic Games and Markov Automata

Autor: Luis María Ferrer Fioriti, Holger Hermanns, Ralf Wimmer, Bettina Braitling, Bernd Becker, Hassan Hatefi

Publikováno v: Dependable Software Engineering: Theories, Tools, and Applications ISBN: 9783319259413
SETTA

Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rew

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::b441710ceec329a4847fb68cbbf5b993
https://doi.org/10.1007/978-3-319-25942-0_2