Skip to main content
SpringerLink
Log in

Qualitative Reachability for Open Interval Markov Chains

  • Conference paper
  • First Online:
Reachability Problems (RP 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11123))

Included in the following conference series:

Abstract

Interval Markov chains extend classical Markov chains with the possibility to describe transition probabilities using intervals, rather than exact values. While the standard formulation of interval Markov chains features closed intervals, previous work has considered also open interval Markov chains, in which the intervals can also be open or half-open. In this paper we focus on qualitative reachability problems for open interval Markov chains, which consider whether the optimal (maximum or minimum) probability with which a certain set of states can be reached is equal to 0 or 1. We present polynomial-time algorithms for these problems for both of the standard semantics of interval Markov chains. Our methods do not rely on the closure of open intervals, in contrast to previous approaches for open interval Markov chains, and can characterise situations in which probability 0 or 1 can be attained not exactly but arbitrarily closely.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Readers familiar with \(\mu \)-calculus will observe that the algorithm can be expressed using the term \(\nu Y\, . \,\mu X(T\cup \mathsf {APre}(Y,X))\) [10].

References

  1. Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. Handbook of Model Checking, pp. 963–999. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_28

    Chapter  MATH  Google Scholar 

  2. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  3. Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Constraint Markov chains. Theor. Comput. Sci. 412(34), 4373–4404 (2011)

    Article  MathSciNet  Google Scholar 

  4. Chakraborty, S., Katoen, J.-P.: Model checking of open interval Markov chains. In: Gribaudo, M., Manini, D., Remke, A. (eds.) ASMTA 2015. LNCS, vol. 9081, pp. 30–42. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-18579-8_3

    Chapter  Google Scholar 

  5. Chatterjee, K., Sen, K., Henzinger, T.A.: Model-checking \(\omega \)-regular properties of interval Markov chains. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 302–317. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78499-9_22

    Chapter  MATH  Google Scholar 

  6. Chen, T., Han, T., Kwiatkowska, M.: On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett. 113(7), 210–216 (2013)

    Article  MathSciNet  Google Scholar 

  7. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)

    Article  MathSciNet  Google Scholar 

  8. Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280–294. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31862-0_21

    Chapter  MATH  Google Scholar 

  9. de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, Department of Computer Science (1997)

    Google Scholar 

  10. Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66–81. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48320-9_7

    Chapter  Google Scholar 

  11. Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21455-4_3

    Chapter  Google Scholar 

  12. Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111–131 (2018)

    Article  MathSciNet  Google Scholar 

  13. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)

    Article  Google Scholar 

  14. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: 1991 Proceedings of LICS, pp. 266–277. IEEE Computer Society (1991)

    Google Scholar 

  15. Kozine, I.O., Utkin, L.V.: Interval-valued finite Markov chains. Reliable Comput. 8(2), 97–113 (2002)

    Article  MathSciNet  Google Scholar 

  16. Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Aspects Comput. 19(1), 93–109 (2007)

    Article  Google Scholar 

  17. Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527–542. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_35

    Chapter  Google Scholar 

  18. Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006). https://doi.org/10.1007/11691372_26

    Chapter  MATH  Google Scholar 

  19. Sproston, J.: Probabilistic timed automata with clock-dependent probabilities. In: Hague, M., Potapov, I. (eds.) RP 2017. LNCS, vol. 10506, pp. 144–159. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67089-8_11

    Chapter  Google Scholar 

  20. Sproston, J.: Qualitative reachability for open interval Markov chains. CoRR (2018)

    Google Scholar 

  21. Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: 1985 Proceedings of FOCS, pp. 327–338. IEEE Computer Society (1985)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, University of Turin, Turin, Italy

    Jeremy Sproston

Authors
  1. Jeremy Sproston
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jeremy Sproston .

Editor information

Editors and Affiliations

  1. University of Liverpool, Liverpool, UK

    Igor Potapov

  2. Aix-Marseille University, Marseille, France

    Pierre-Alain Reynier

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Sproston, J. (2018). Qualitative Reachability for Open Interval Markov Chains. In: Potapov, I., Reynier, PA. (eds) Reachability Problems. RP 2018. Lecture Notes in Computer Science(), vol 11123. Springer, Cham. https://doi.org/10.1007/978-3-030-00250-3_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-00250-3_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-00249-7

  • Online ISBN: 978-3-030-00250-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation