Advertisement

Prinsys—On a Quest for Probabilistic Loop Invariants

  • Friedrich Gretz
  • Joost-Pieter Katoen
  • Annabelle McIver
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)

Abstract

Prinsys (pronounced “princess”) is a new software-tool for probabilistic invariant synthesis. In this paper we discuss its implementation and improvements of the methodology which was set out in previous work. In particular we have substantially simplified the method and generalised it to non-linear programs and invariants. Prinsys follows a constraint-based approach. A given parameterised loop annotation is speculatively placed in the program. The tool returns a formula that captures precisely the invariant instances of the given candidate. Our approach is sound and complete. Prinsys’s applicability is evaluated on several examples. We believe the tool contributes to the successful analysis of sequential probabilistic programs with infinite-domain variables and parameters.

Keywords

invariant generation probabilistic programs non-linear constraint solving 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Barthe, G., Grégoire, B., Béguelin, S.Z.: Probabilistic relational Hoare logics for computer-aided security proofs. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol. 7342, pp. 1–6. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    Barthe, G., Köpf, B., Olmedo, F., Béguelin, S.Z.: Probabilistic relational reasoning for differential privacy. In: Symp. on Principles of Programming Languages (POPL), pp. 97–110. ACM (2012)Google Scholar
  3. 3.
    Gretz, F.: Invariant Generation for Linear Probabilistic Programs. Master’s thesis, RWTH Aachen (2010), http://www-i2.informatik.rwth-aachen.de/i2/gretz/
  4. 4.
    Gretz, F., Katoen, J.P., McIver, A.: Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language. In: QEST, pp. 168–177 (2012)Google Scholar
  5. 5.
    Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: Abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 353–357. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic Reachability for Parametric Markov Models. STTT 13(1), 3–19 (2011)CrossRefGoogle Scholar
  7. 7.
    Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-Invariant Generation for Probabilistic Programs: In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390–406. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  8. 8.
    Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: On the Complexity of the Equivalence Problem for Probabilistic Automata. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 467–481. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  9. 9.
    Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: APEX: An Analyzer for Open Probabilistic Programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 693–698. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    McIver, A., Morgan, C.: Abstraction, Refinement and Proof For Probabilistic Systems. Monographs in Computer Science. Springer (2004)Google Scholar
  12. 12.
    Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear Loop Invariant Generation Using Gröbner Bases. In: POPL, pp. 318–329 (2004)Google Scholar
  13. 13.
    Ying, M.: Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6), 19 (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Friedrich Gretz
    • 1
    • 2
  • Joost-Pieter Katoen
    • 1
  • Annabelle McIver
    • 2
  1. 1.RWTH Aachen UniversityGermany
  2. 2.Macquarie UniversityAustralia

Personalised recommendations