Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Robots at the Edge of the Cloud Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Probabilistic CTL\(^{*}\): The Deductive Way

Authors : Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns, Rupak Majumdar

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Complex probabilistic temporal behaviours need to be guaranteed in robotics and various other control domains, as well as in the context of families of randomized protocols. At its core, this entails checking infinite-state probabilistic systems with respect to quantitative properties specified in probabilistic temporal logics. Model checking methods are not directly applicable to infinite-state systems, and techniques for infinite-state probabilistic systems are limited in terms of the specifications they can handle.
This paper presents a deductive approach to the verification of countable-state systems against properties specified in probabilistic CTL\(^{*}\), on models featuring both nondeterministic and probabilistic choices. The deductive proof system we propose lifts the classical proof system by Kesten and Pnueli to the probabilistic setting. However, the soundness arguments are completely distinct and go via the theory of martingales. Completeness results for the finite-state case and an infinite-state example illustrate the effectiveness of our approach.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Deductive Proofs of Almost Sure Persistence and Recurrence Properties
next chapter Parametric Runtime Verification of C Programs
Footnotes
1
Usually, path formulas in PCTL\(^*\) are defined using linear temporal logic (LTL) [2]. Since the analysis of PCTL\(^*\) proceeds by first converting LTL to a deterministic automaton, we omit the intermediate step of converting LTL to automata and assume the path formulas are given as deterministic Streett automata.
 
Literature
1.
Arons, T., Pnueli, A., Zuck, L.D.: Parameterized verification by probabilistic abstraction. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 87–102. Springer, Heidelberg (2003)CrossRef
2.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
3.
4.
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS. LNCS, pp. 499–513. Springer, Heidelberg (1995)CrossRef
5.
Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 323–337. Springer, Heidelberg (2005)CrossRef
6.
Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511–526. Springer, Heidelberg (2013)CrossRef
7.
8.
de Alfaro, L.: Formal verification of probabilistic systems. PhD thesis, Standford (1997)
9.
de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, p. 395. Springer, Heidelberg (2000)CrossRef
10.
Dimitrova, R., Ferrer Fioriti, L.M., Hermanns, H., Majumdar, R.: PCTL\(^*\): the deductive way (extended version). Reports of SFB/TR 14 AVACS 114, (2016). http://​www.​avacs.​org
11.
Durrett, R.: Probability: Theory and Examples. Series in Statistical and Probabilistic Mathematics, 4th edn. Cambridge University Press, New York (2010)CrossRefMATH
12.
Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 123–138. Springer, Heidelberg (2012)CrossRef
13.
Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL, pp. 489–501 (2015)
14.
Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1997)MATH
15.
Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer, Heidelberg (1986)CrossRefMATH
16.
Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst. 5(3), 356–380 (1983)CrossRefMATH
17.
Hurd, J.: Formal verification of probabilistic algorithms. PhD thesis, University of Cambridge (2001)
18.
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)CrossRef
19.
20.
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic model checking for performance and reliability analysis. SIGMETRICS Perform. Eval. Rev. 36(4), 40–45 (2009)CrossRef
21.
McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005)MATH
22.
Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pp. 278–290 (1983)
23.
24.
25.
Slanina, M., Sipma, H.B., Manna, Z.: Deductive verification of alternating systems. Form. Asp. Comput. 20(4–5), 507–560 (2008)CrossRefMATH
26.
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338 (1985)
Metadata
Title
Probabilistic CTL: The Deductive Way
Authors
Rayna Dimitrova
Luis María Ferrer Fioriti
Holger Hermanns
Rupak Majumdar
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Tools and Algorithms for the Construction and Analysis of Systems

Print ISBN: 978-3-662-49673-2

Electronic ISBN: 978-3-662-49674-9

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-662-49674-9_16

Premium Partner

    Image Credits