Advertisement

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

  • Tomáš Brázdil
  • Krishnendu Chatterjee
  • Antonín Kučera
  • Petr Novotný
  • Dominik VelanEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11781)

Abstract

A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in \(\varOmega (n^2)\).

Keywords

Angelic and demonic nondeterminism Termination time Probabilistic VASS 

References

  1. 1.
    de Alfaro, L.: Formal verification of probabilistic systems. Phd. thesis, Stanford University, Stanford, CA, USA (1998)Google Scholar
  2. 2.
    Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness of parameterized timed networks. In: Proceedings of ICALP 2015, pp. 375–387 (2015)CrossRefGoogle Scholar
  3. 3.
    Atig, M.F., Habermehl, P.: On yen’s path logic for petri nets. Int. J. Found. Comput. Sci. 22(04), 783–799 (2011)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)zbMATHGoogle Scholar
  5. 5.
    Barthe, G., Gaboardi, M., Grégoire, B., Hsu, J., Strub, P.Y.: Proving differential privacy via probabilistic couplings. In: Proceedings of LICS 2016. pp. 749–758. ACM, New York (2016)Google Scholar
  6. 6.
    Bloem, R., et al.: Decidability in parameterized verification. SIGACT News 47(2), 53–64 (2016)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Bozzelli, L., Ganty, P.: Complexity analysis of the backward coverability algorithm for VASS. In: Proceedings of RP 2011, pp. 96–109 (2011)Google Scholar
  8. 8.
    Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., Kučera, A.: Markov decision processes with multiple long-run average objectives. 10(1), 1–29 (2014)Google Scholar
  9. 9.
    Brázdil, T., Brožek, V., Etessami, K., Kučera, A.: Approximating the termination value of one-counter MDPs and Stochastic games. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 332–343. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22012-8_26 CrossRefzbMATHGoogle Scholar
  10. 10.
    Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P., Velan, D., Zuleger, F.: Efficient algorithms for asymptotic bounds on termination time in VASS. In: Proceedings of LICS 2018, pp. 185–194 (2018)Google Scholar
  11. 11.
    Brázdil, T., Kiefer, S., Kučera, A.: Efficient analysis of probabilistic programs with an unbounded counter. J. ACM 61(6) (2014)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Brázdil, T., Kučera, A., Novotný, P., Wojtczak, D.: Minimizing Expected termination time in one-counter Markov decision processes. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012. LNCS, vol. 7392, pp. 141–152. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31585-5_16CrossRefGoogle Scholar
  13. 13.
    Cassez, F.: Timed games for computing WCET for pipelined processors with caches. In: 2011 Eleventh International Conference on Application of Concurrency to System Design, pp. 195–204, (June 2011)Google Scholar
  14. 14.
    Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.F.: Generalized mean-payoff and energy games. In: Proceedings of FSTTCS 2010, pp. 505–516 (2010)Google Scholar
  15. 15.
    Chatterjee, K., Velner, Y.: Hyperplane separation technique for multidimensional mean-payoff games. In: Proceedings of CONCUR 2013, pp. 500–515 (2013)CrossRefGoogle Scholar
  16. 16.
    Chatterjee, K., Fu, H., Goharshady, A.K.: Non-polynomial worst-case analysis of recursive programs. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 41–63. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_3CrossRefGoogle Scholar
  17. 17.
    Chatterjee, K., Fu, H., Murhekar, A.: Automated recurrence analysis for almost-linear expected-runtime bounds. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 118–139. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63387-9_6CrossRefGoogle Scholar
  18. 18.
    Colcombet, T., Jurdzinski, M., Lazic, R., Schmitz, S.: Perfect half space games. In: Proceedings of LICS 2017, pp. 1–11 (2017)Google Scholar
  19. 19.
    Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for petri nets is not elementary. In: Proceedings of STOC 2019, pp. 24–33 (2019)Google Scholar
  20. 20.
    Esparza, J.: Decidability and complexity of Petri net problems—an introduction. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998).  https://doi.org/10.1007/3-540-65306-6_20CrossRefzbMATHGoogle Scholar
  21. 21.
    Esparza, J., Kučera, A., Mayr, R.: Model-checking probabilistic pushdown automata. 2(1:2), 1–31 (2006)Google Scholar
  22. 22.
    Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An smt-based approach to coverability analysis. In: Proceedings of CAV 2014, pp. 603–619 (2014)CrossRefGoogle Scholar
  23. 23.
    Esparza, J., Nielsen, M.: Decidability issues for petri nets - a survey. Bull. EATCS 52, 245–262 (1994)zbMATHGoogle Scholar
  24. 24.
    Etessami, K., Yannakakis, M.: Model checking of recursive probabilistic systems. ACM Trans. Comput. Log. 13, 12 (2012)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 282–309. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49498-1_12CrossRefGoogle Scholar
  26. 26.
    Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nature 521(7553), 452–459 (2015)CrossRefGoogle Scholar
  27. 27.
    Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. In: Proceedings of POPL 2009. pp. 127–139. ACM, New York (2009)CrossRefGoogle Scholar
  28. 28.
    Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Prog. Lang. Syst. 34(3), 14:1–14:62 (2012)CrossRefGoogle Scholar
  29. 29.
    Jurdzinski, M., Lazic, R., Schmitz, S.: Fixed-dimensional energy games are in pseudo-polynomial time. In: Proceedings of ICALP 2015, pp. 260–272 (2015)CrossRefGoogle Scholar
  30. 30.
    Kaminski, B.L., Katoen, J., Matheja, C.: On the hardness of analyzing probabilistic programs. Acta Inf. 56(3), 255–285 (2019)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1–30:68 (2018)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of STOC 1982, pp. 267–281. ACM (1982)Google Scholar
  34. 34.
    Kosaraju, S.R., Sullivan, G.F.: Detecting cycles in dynamic graphs in polynomial time. In: Proceedings of STOC 1988, pp. 398–406 (1988)Google Scholar
  35. 35.
    Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: Proceedings of POPL 2011, pp. 307–316 (2011)CrossRefGoogle Scholar
  36. 36.
    Leroux, J.: Polynomial vector addition systems with states. In: Proceedings of ICALP 2018, vol. 107, pp. 134:1–134:13 (2018)Google Scholar
  37. 37.
    Leroux, J., Schmitz, S.: Reachability in vector addition systems is primitive-recursive in fixed dimension. In: Proceedings of LICS 2019 (2019)Google Scholar
  38. 38.
    Lipton, R.: The reachability problem requires exponential space. Technical Report 62 (1976)Google Scholar
  39. 39.
    Mayr, E.: An algorithm for the general Petri net reachability problem. SIAM J. Comput. 13, 441–460 (1984)MathSciNetCrossRefGoogle Scholar
  40. 40.
    Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: Resource analysis for probabilistic programs. In: Proceedings of PLDI 2018, pp. 496–512. ACM, New York (2018)CrossRefGoogle Scholar
  41. 41.
    Puterman, M.: Markov Decision Processes (1994)Google Scholar
  42. 42.
    Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978)MathSciNetCrossRefGoogle Scholar
  43. 43.
    Schmitz, S.: Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory 8(1), 3:1–3:36 (2016)MathSciNetCrossRefGoogle Scholar
  44. 44.
    Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Proccedings of CAV 2014, pp. 745–761 (2014)CrossRefGoogle Scholar
  45. 45.
    Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics (Intelligent Robotics and Autonomous Agents). The MIT Press, Cambridge (2005)zbMATHGoogle Scholar
  46. 46.
    Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A.M., Raskin, J.: The complexity of multi-mean-payoff and multi-energy games. Inf. Comput. 241, 177–196 (2015)MathSciNetCrossRefGoogle Scholar
  47. 47.
    Wilhelm, R., et al.: The worst-case execution-time problem—overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7(3), 36:1–36:53 (2008)CrossRefGoogle Scholar
  48. 48.
    Yen, H.C.: A unified approach for deciding the existence of certain petri net paths. Inf. Comput. 96(1), 119–137 (1992)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Tomáš Brázdil
    • 1
  • Krishnendu Chatterjee
    • 2
  • Antonín Kučera
    • 1
  • Petr Novotný
    • 1
  • Dominik Velan
    • 1
    Email author
  1. 1.Faculty of InformaticsMasaryk UniversityBrnoCzech Republic
  2. 2.IST AustriaKlosterneuburgAustria

Personalised recommendations