Advertisement

Convex Language Semantics for Nondeterministic Probabilistic Automata

  • Gerco van Heerdt
  • Justin Hsu
  • Joël Ouaknine
  • Alexandra Silva
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)

Abstract

We explore language semantics for automata combining probabilistic and nondeterministic behaviors. We first show that there are precisely two natural semantics for probabilistic automata with nondeterminism. For both choices, we show that these automata are strictly more expressive than deterministic probabilistic automata, and we prove that the problem of checking language equivalence is undecidable by reduction from the threshold problem. However, we provide a discounted metric that can be computed to arbitrarily high precision.

Notes

Acknowledgements

We thank Nathanaël Fijalkow and the anonymous reviewers for their useful suggestions to improve the paper. The semantics studied in this paper has been brought to our attention in personal communication by Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Their interest in this semantics is mostly motivated by its relationship with trace semantics previously proposed in the literature. This is the subject of a forthcoming publication [8].

References

  1. 1.
    Akshay, S., Antonopoulos, T., Ouaknine, J., Worrell, J.: Reachability problems for Markov chains. Inf. Process. Lett. 115(2), 155–158 (2015).  https://doi.org/10.1016/j.ipl.2014.08.013MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Arbib, M.A., Manes, E.G.: Fuzzy machines in a category. Bull. Aust. Math. Soc. 13(2), 169–210 (1975).  https://doi.org/10.1017/s0004972700024412MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Balle, B., Castro, J., Gavaldà, R.: Adaptively learning probabilistic deterministic automata from data streams. Mach. Learn. 96(1–2), 99–127 (2014).  https://doi.org/10.1007/s10994-013-5408-xMathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. Log. Methods Comput. Sci. 10(1), Article no. 16 (2014).  https://doi.org/10.2168/lmcs-10(1:16)2014
  5. 5.
    Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension. Theory Comput. Syst. 36, 231–245 (2003).  https://doi.org/10.1007/s00224-003-1061-2MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun. ACM 58(2), 87–95 (2015).  https://doi.org/10.1145/2713167CrossRefGoogle Scholar
  7. 7.
    Bonchi, F., Silva, A., Sokolova, A.: The power of convex algebras. In: Meyer, R., Nestmann, U. (eds.) Proceedings of 28th International Conference on Concurrency Theory, CONCUR 2017, Berlin, September 2017. Leibniz International Proceedings in Informatics, vol. 85, Article no. 23. Dagstuhl Publishing, Saarbrücken/Wadern (2017).  https://doi.org/10.4230/lipics.concur.2017.23
  8. 8.
    Bonchi, F., Sokolova, A., Vignudelli, V.: Trace semantics for nondeterministic probabilistic automata via determinization. arXiv preprint 1808.00923 (2018). https://arxiv.org/abs/1808.00923
  9. 9.
    Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 274–288. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04081-8_19CrossRefGoogle Scholar
  10. 10.
    Desharnais, J., Edalat, A., Panangaden, P.: A logical characterization of bisimulation for labeled Markov processes. In: Proceedings of 13th Annual IEEE Symposium on Logic in Computer Science. LICS 1998, Indianapolis, IN, June 1998, pp. 478–487. IEEE CS Press, Washington, D.C. (1998).  https://doi.org/10.1109/lics.1998.705681
  11. 11.
    Everest, G., van der Poorten, A.J., Shparlinski, I.E., Ward, T.: Recurrence Sequences, Mathematical surveys and monographs, vol. 104. American Mathematical Society, Providence (2003)CrossRefGoogle Scholar
  12. 12.
    Fijalkow, N.: Undecidability results for probabilistic automata. ACM SIGLOG News 4(4), 10–17 (2017).  https://doi.org/10.1145/3157831.3157833CrossRefGoogle Scholar
  13. 13.
    Fijalkow, N., Klin, B., Panangaden, P.: Expressiveness of probabilistic modal logics, revisited. In: Chatzigiannakis, Y., Indyk, P., Kuhn, F., Muscholl, A. (eds.) Proc. of 44th Int. Coll. on Automata, Languages and Programming, ICALP 2017, Warsaw, July 2017. Leibniz International Proceedings in Informatics, vol. 80, Article no. 105. Dagstuhl Publishing, Saarbrücken/Wadern (2017).  https://doi.org/10.4230/lipics.icalp.2017.105
  14. 14.
    Goncharov, S., Milius, S., Silva, A.: Towards a coalgebraic Chomsky hierarchy (extended abstract). In: Díaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 265–280. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44602-7_21CrossRefGoogle Scholar
  15. 15.
    Henzinger, T.A.: Quantitative reactive modeling and verification. Comput. Sci. Res. Dev. 28(4), 331–344 (2013).  https://doi.org/10.1007/s00450-013-0251-7CrossRefGoogle Scholar
  16. 16.
    Hermanns, H., Katoen, J.: The how and why of interactive Markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 311–337. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17071-3_16CrossRefzbMATHGoogle Scholar
  17. 17.
    Hermanns, H., Krcál, J., Kretínský, J.: Probabilistic bisimulation: naturally on distributions. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 249–265. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44584-6_18CrossRefGoogle Scholar
  18. 18.
    Kozen, D.: Semantics of probabilistic programs. In: Proceedings of 20th Annual Symposium on Foundations of Computer Science, FOCS 1979, San Juan, PR, October 1979, pp. 101–114. IEEE CS Press, Washington, D.C. (1979).  https://doi.org/10.1109/sfcs.1979.38
  19. 19.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  20. 20.
    Legay, A., Murawski, A.S., Ouaknine, J., Worrell, J.: On automated verification of probabilistic programs. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 173–187. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_13CrossRefGoogle Scholar
  21. 21.
    Ouaknine, J., Worrell, J.: Positivity problems for low-order linear recurrence sequences. In: Proceedings of 25th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, OR, January 2014, pp. 366–379. SIAM (2014).  https://doi.org/10.1137/1.9781611973402zbMATHGoogle Scholar
  22. 22.
    Paz, A.: Introduction to Probabilistic Automata. Academic Press, New York/London (1971).  https://doi.org/10.1016/c2013-0-11297-4CrossRefzbMATHGoogle Scholar
  23. 23.
    Rabin, M.O.: Probabilistic automata. Inf. Control 6(3), 230–245 (1963).  https://doi.org/10.1016/s0019-9958(63)90290-0MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Rabin, M.O.: Probabilistic algorithms. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 21–39. Academic Press, New York (1976)Google Scholar
  25. 25.
    Rabin, M.O.: \(N\)-process mutual exclusion with bounded waiting by \(4 \log _2 N\)-valued shared variable. J. Comput. Syst. Sci. 25(1), 66–75 (1982).  https://doi.org/10.1016/0022-0000(82)90010-1CrossRefzbMATHGoogle Scholar
  26. 26.
    Ron, D., Singer, Y., Tishby, N.: The power of amnesia: learning probabilistic automata with variable memory length. Mach. Learn. 25(2), 117–149 (1996).  https://doi.org/10.1023/a:1026490906255CrossRefzbMATHGoogle Scholar
  27. 27.
    Sassone, V., Nielsen, M., Winskel, G.: Models for concurrency: towards a classification. Theor. Comput. Sci. 170(1–2), 297–348 (1996).  https://doi.org/10.1016/s0304-3975(96)80710-9MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge (1995)Google Scholar
  29. 29.
    Silva, A., Bonchi, F., Bonsangue, M.M., Rutten, J.J.M.M.: Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci. 9(1), Article no. 9 (2013).  https://doi.org/10.2168/lmcs-9(1:9)2013
  30. 30.
    Swaminathan, M., Katoen, J.P., Olderog, E.R.: Layered reasoning for randomized distributed algorithms. Form. Asp. Comput. 24(4), 477–496 (2012).  https://doi.org/10.1007/s00165-012-0231-xMathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Vardi, M.Y.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  32. 32.
    Vignudelli, V.: Behavioral equivalences for higher-order languages with probabilities. Ph.D. thesis, Univ. di Bologna (2017)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Gerco van Heerdt
    • 1
  • Justin Hsu
    • 2
  • Joël Ouaknine
    • 3
    • 4
  • Alexandra Silva
    • 1
  1. 1.Department of Computer ScienceUniversity College LondonLondonUK
  2. 2.Department of Computer SciencesUniversity of Wisconsin-MadisonMadisonUSA
  3. 3.Max Planck Institute for Software SystemsSaarbrückenGermany
  4. 4.Department of Computer ScienceOxford UniversityOxfordUK

Personalised recommendations