Document Open Access Logo

Consistency for Parametric Interval Markov Chains

Author Benoît Delahaye

PDF
Thumbnail PDF

File

OASIcs.SynCoP.2015.17.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Author Details

Benoît Delahaye

Cite AsGet BibTex

Benoît Delahaye. Consistency for Parametric Interval Markov Chains. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 17-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/OASIcs.SynCoP.2015.17

Abstract

Interval Markov Chains (IMCs) are the base of a classic probabilistic specification theory by Larsen and Jonsson in 1991. They are also a popular abstraction for probabilistic systems. In this paper we introduce and study an extension of Interval Markov Chains with parametric intervals. In particular, we investigate the consistency problem for such models and propose an efficient solution for the subclass of parametric IMCs with local parameters only. We also show that this problem is still decidable for parametric IMCs with global parameters, although more complex in this case.
Keywords
  • Specification
  • Parameters
  • Markov Chains
  • Consistency

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. É. André, L. Fribourg, and J. Sproston. An extension of the inverse method to probabilistic timed automata. Formal Methods in System Design, (2):119-145, 2013. Google Scholar
  2. R. Barbuti, F. Levi, P. Milazzo, and G. Scatena. Probabilistic model checking of biological systems with uncertain kinetic rates. Theor. Comput. Sci., 419(0):2 - 16, 2012. Google Scholar
  3. N. Bertrand and P. Fournier. Parameterized verification of many identical probabilistic timed processes. In FSTTCS, volume 24 of LIPIcs, pages 501-513, 2013. Google Scholar
  4. N. Bertrand, P. Fournier, and A. Sangnier. Playing with probabilities in reconfigurable broadcast networks. In FoSSaCS, volume 8412 of LNCS, pages 134-148. Springer, 2014. Google Scholar
  5. F. Biondi, A. Legay, B.F. Nielsen, and A. Wasowski. Maximizing entropy over markov processes. In LATA, volume 7810 of LNCS, pages 128-140. Springer, 2013. Google Scholar
  6. B. Caillaud, B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, and A. Wasowski. Constraint markov chains. Theor. Comput. Sci., 412(34):4373-4404, 2011. Google Scholar
  7. N. Chamseddine, M. Duflot, L. Fribourg, C. Picaronny, and J. Sproston. Computing expected absorption times for parametric determinate probabilistic timed automata. In QEST, pages 254-263. IEEE Computer Society, 2008. Google Scholar
  8. C. Daws. Symbolic and parametric model checking of discrete-time Markov chains. In ICTAC, volume 3407 of LNCS, pages 280-294. Springer, 2004. Google Scholar
  9. B. Delahaye, J-P. Katoen, K.G. Larsen, A. Legay, M.L. Pedersen, F. Sher, and A. Wasowski. Abstract probabilistic automata. Inf. Comput., 232:66-116, 2013. Google Scholar
  10. B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, and A. Wasowski. Consistency and refinement for interval markov chains. J. Log. Algebr. Program., 81(3):209-226, 2012. Google Scholar
  11. L.M. Ferrer Fioriti, E.M. Hahn, H. Hermanns, and B. Wachter. Variable probabilistic abstraction refinement. In ATVA, volume 7561 of LNCS, pages 300-316. Springer, 2012. Google Scholar
  12. R. Gori and F. Levi. An analysis for proving probabilistic termination of biological systems. Theor. Comput. Sci., 471(0):27 - 73, 2013. Google Scholar
  13. E.M. Hahn, T. Han, and L. Zhang. Synthesis for PCTL in parametric Markov decision processes. In NSFM, volume 6617 of LNCS, pages 146-161. Springer, 2011. Google Scholar
  14. E.M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. PARAM: A model checker for parametric Markov models. In CAV, volume 6174 of LNCS, pages 660-664. Springer, 2010. Google Scholar
  15. E.M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. Software Tools for Technology Transfer, 13(1):3-19, 2011. Google Scholar
  16. B. Jonsson and K.G. Larsen. Specification and refinement of probabilistic processes. In LICS, pages 266-277. IEEE Computer, 1991. Google Scholar
  17. R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Decidability results for parametric probabilistic transition systems with an application to security. In SEFM, pages 114-121. IEEE Computer Society, 2004. Google Scholar
  18. R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Parametric probabilistic transition systems for system design and analysis. Formal Aspects of Computing, 19(1):93-109, 2007. Google Scholar
  19. K. Sen, M. Viswanathan, and G. Agha. Model-checking markov chains in the presence of uncertainties. In TACAS, volume 3920 of LNCS, pages 394-410. Springer, 2006. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact