Advertisement

Refinement and Difference for Probabilistic Automata

  • Benoît Delahaye
  • Uli Fahrenberg
  • Kim Guldstrand Larsen
  • Axel Legay
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)

Abstract

This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of this failure. Our contribution is an algorithm that allows to approximate the difference of two deterministic APAs with arbitrary precision. Our technique relies on new quantitative notions of distances between APAs used to assess convergence of the approximations as well as on an in-depth inspection of the refinement relation for APAs. The procedure is effective and not more complex than refinement checking.

Keywords

Model Check Atomic Proposition Bound Model Check State Space Explosion Probabilistic Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aliprantis, C.D., Border, K.C.: Infinite Dimensional Analysis: A Hitchhiker’s Guide, 3rd edn. Springer (2007)Google Scholar
  2. 2.
    Aljazzar, H., Leue, S.: Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans. Software Eng. (2010)Google Scholar
  3. 3.
    Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Andrés, M.E., D’Argenio, P., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 129–148. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  5. 5.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)Google Scholar
  6. 6.
    Bauer, S.S., Fahrenberg, U., Legay, A., Thrane, C.: General quantitative specification theories with modalities. In: Hirsch, E.A., Karhumäki, J., Lepistö, A., Prilutskii, M. (eds.) CSR 2012. LNCS, vol. 7353, pp. 18–30. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  7. 7.
    Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Constraint Markov chains. TCS 412(34), 4373–4404 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Trans. Comput. Log. 12(1), 1 (2010)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2) (2008)Google Scholar
  10. 10.
    Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: FSE, pp. 109–120. ACM (2001)Google Scholar
  12. 12.
    de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game relations and metrics. In: LICS, pp. 99–108. IEEE Computer Society (2007)Google Scholar
  13. 13.
    Delahaye, B., Fahrenberg, U., Larsen, K.G., Legay, A.: Refinement and difference for probabilistic automata - long version (2013), http://delahaye.benoit.free.fr/rapports/QEST13-long.pdf
  14. 14.
    Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  15. 15.
    Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: New results on abstract probabilistic automata. In: ACSD, pp. 118–127. IEEE (2011)Google Scholar
  16. 16.
    Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: APAC: A tool for reasoning about abstract probabilistic automata. In: QEST, pp. 151–152. IEEE (2011)Google Scholar
  17. 17.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. TCS 318(3), 323–354 (2004)MathSciNetzbMATHCrossRefGoogle Scholar
  18. 18.
    Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
    Han, T., Katoen, J.-P., Damman, B.: Counterexample generation in probabilistic model checking. IEEE Trans. Software Eng. 35(2), 241–257 (2009)CrossRefGoogle Scholar
  20. 20.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994)zbMATHCrossRefGoogle Scholar
  21. 21.
    Hermanns, H., Herzog, U., Katoen, J.: Process algebra for performance evaluation. TCS 274(1-2), 43–87 (2002)MathSciNetzbMATHCrossRefGoogle Scholar
  22. 22.
    Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162–175. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  24. 24.
    Jansen, N., Ábrahám, E., Katelaan, J., Wimmer, R., Katoen, J.-P., Becker, B.: Hierarchical counterexamples for discrete-time Markov chains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 443–452. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  25. 25.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE (1991)Google Scholar
  26. 26.
    Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  27. 27.
    Komuravelli, A., Păsăreanu, C.S., Clarke, E.M.: Assume-guarantee abstraction refinement for probabilistic systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 310–326. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  28. 28.
    Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 23–37. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  29. 29.
    Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  30. 30.
    Larsen, K.G., Fahrenberg, U., Thrane, C.: Metrics for weighted transition systems: Axiomatization and complexity. TCS 412(28), 3358–3369 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  31. 31.
    Lynch, N., Tuttle, M.R.: An introduction to Input/Output automata. CWI 2(3) (1989)Google Scholar
  32. 32.
    Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)Google Scholar
  33. 33.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer (1992)Google Scholar
  34. 34.
    Raclet, J.-B.: Quotient de spécifications pour la réutilisation de composants. PhD thesis, Université de Rennes I (December 2007) (in French)Google Scholar
  35. 35.
    Sassolas, M., Chechik, M., Uchitel, S.: Exploring inconsistencies between modal transition systems. Software and System Modeling 10(1), 117–142 (2011)CrossRefGoogle Scholar
  36. 36.
    Schmalz, M., Varacca, D., Völzer, H.: Counterexamples in probabilistic LTL model checking for Markov chains. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 587–602. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  37. 37.
    Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  38. 38.
    Sher, F., Katoen, J.-P.: Compositional abstraction techniques for probabilistic automata. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 325–341. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  39. 39.
    Thrane, C., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. JLAP 79(7), 689–703 (2010)MathSciNetzbMATHGoogle Scholar
  40. 40.
    van Breugel, F., Mislove, M.W., Ouaknine, J., Worrell, J.: An intrinsic characterization of approximate probabilistic bisimilarity. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 200–215. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  41. 41.
    Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338. IEEE (1985)Google Scholar
  42. 42.
    Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time Markov chains using bounded model checking. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 366–380. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  43. 43.
    Wimmer, R., Jansen, N., Ábrahám, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time Markov models. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299–314. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Benoît Delahaye
    • 1
  • Uli Fahrenberg
    • 1
  • Kim Guldstrand Larsen
    • 2
  • Axel Legay
    • 1
  1. 1.INRIA/IRISAFrance
  2. 2.Aalborg UniversityDenmark

Personalised recommendations