Validierung Stochastischer Systeme

Inhalt

Traditionally, the area of model-based performance and dependability evaluation and the area of formal specification and verification of systems have been approached completely independently of each other. However, increasingly, system properties related to performance and dependability cannot be seen separately from issues concerning the formal correctness of systems, that is, the notion of "correctness" includes aspects of both performance and dependability. Therefore, a separate treatment of these system aspects becomes less appropriate.

Over the last few years, good progress has been made in combining techniques from these previously separate fields. Active areas of research are model-checking procedures for stochastically timed systems and deductive verification techniques in which time bounds play a role. However, all these results are currently only available in state-of-the-art research literature, and, moreover, spread over journals and conferences of different research communities. It goes without saying that there are currently no textbooks available on this subject. Hence, to obtain a good overview of the important results and about the open research topics in this area, a structured review of the literature seems most appropriate and timely.

Veranstalter

Prof. Dr. Joost-Pieter Katoen
Tel. 0241/80-21207
Raum 4232

Vorbesprechung

Am 26.01.2005 fand eine Vorbesprechung statt.

Folien zur Vorbesprechung

Termine

Zuordnung

Voraussetzungen

• Automatentheorie
• Model Checking
• Wahrscheinlichkeitstheorie
• Leistungsbewertung

Rückfragen

Themen und Literatur

1. Diskret-kontinuierliche Markov Ketten (DTMC)
   • H.C. Tijms: A First Course on Stochastic Models. Jon Wiley, 2003. [Kapitel 3]
   • B. R. Haverkort: Performance of Computer Communication Systems. John Wiley & Sons, 1998. [Kapitel 3.1-3.4]
2. Zeit-kontinuierliche Markov Ketten (CTMC)
   • B.R. Haverkort: Performance and Dependability Modelling with CTMCs. LNCS 2090, 2001.
   • H.C. Tijms: A First Course on Stochastic Models. Jon Wiley, 2003. [Kapitel 4]
   • B. R. Haverkort: Performance of Computer Communication Systems. John Wiley & Sons, 1998. [Kapitel 3.5-3.8]
3. Probabilistische Modelle mit Nichtdeterminismus (MDP)
   • H.C. Tijms: A First Course on Stochastic Models. Jon Wiley, 2003. [Kapitel 6]
   • M.L. Puterman: Markov Decision Processes.
4. Model Checking Probabilistic CTL (1)
   • H. Hansson, B. Jonsson: A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, Vol 6, pp 512-535, 1994.
   • F. Ciesinski, M. Groesser: On Probabilistic CTL. LNCS 2925, pp. 147-188, 2004.
5. Model Checking Probabilistic CTL (2)
   • C. Baier, M. Kwiatkowska: Model Checking for a Probabilistic Branching Time Logic with Fairness. Distributed Computing Vol. 11, 1998.
   • F. Ciesinski, M. Groesser: On Probabilistic CTL. LNCS 2925, pp. 147-188, 2004.
6. Model Checking LTL
   • B. Bollig, M. Leucker: Verifying Qualitative Properties of Probabilistic Programs. LNCS 2925, pp. 124-146, 2004.
   • M. Vardi: Automatic Verification of probabilistic concurrent finite-state programs. Proc. FOCS'85, pp 327-338, 1985.
7. Model Checking 3-valued Probabilistic CTL
   • M. Leucker, V. Wolf: Don't Know in Probabilistic Systems. 2005.
8. Verifikation von Markov Entscheidungsprozessen
   • L. de Alfaro: How to Specify and Verify the Long-Run Average Behavior of Probabilistic Systems. LICS 1998: 454-465
9. Model Checking Continuous Stochastic Logic (1)
   • A. Aziz, V. Singhal, F. Balarin, R. Brayton, A. Sangiovanni-Vincentelli: Model Checking Continuous Time Markov Chains. ACM Trans. on Computational Logic, Vol. 1(1), pp 162-170, 2000.
10. Model Checking Continuous Stochastic Logic (2)
    • C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng. 29(6): 524-541, 2003.
11. Verifikation diskret-kontinuierlicher Markov Ketten mit Kosten
    • S. Andova, H. Hermanns, J.-P. Katoen: Discrete-Time Rewards Model-Checked. FORMATS 2003, LNCS 2791, 88-104, 2003.
12. Verifikation zeit-kontinuierlicher Markov Ketten mit Kosten (1)
    • C. Baier, B. Haverkort, H. Hermanns, J-P. Katoen: On the logical characterisation of performability properties. Automata, Languages and Programming (ICALP 2000), LNCS 1853, pages 780-792, Springer-Verlag, 2000.
    • B. R. Haverkort, L. Cloth, H. Hermanns, J.-P. Katoen, C. Baier: Model Checking Performability Properties. Dependable Systems and Networks 2002: 103-112
13. Verifikation zeit-kontinuierlicher Markov Ketten mit Kosten (2)
    • L. de Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, M. Stoelinga: Model Checking Discounted Temporal Properties. TACAS 2004: 77-92
14. Verifikation von cost-extended Markov Entscheidungsprozessen
    • L. de Alfaro: Computing Minimum and Maximum Reachability Times in Probabilistic Systems. CONCUR 1999: 66-81
15. Verifikation zeit-kontinuierlicher Markov Entscheidungsprozesse
    • C. Baier, B. R. Haverkort, H. Hermanns, J.-P. Katoen: Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes. TACAS 2004: 61-76
16. Partial-Order Reduktion von Markov Entscheidungsprozessen
    • E. Clarke, O. Grumberg and D. Peled: Model Checking. MIT Press, 1999 [Kapitel 10]
    • G. Holzmann: The SPIN Model Checker. 2003 [Kapitel 9, teilweise]
    • C. Baier, F. Ciezinski and M. Größer: Partial Order Reduction for Probabilistic Systems. QEST 2004.
17. Probabilistische Büchi Automaten
    • C. Baier, M. Größer: Recognizing omega-regular languages with probabilistic automata. 2005.
18. Leader election for anonymous rings
    • W.J. Fokkink and J. Pang: Simplifying Itai-Rodeh leader election for anonymous rings. In (M. Huth and S. Uchitel, eds) Proc. 4th Workshop on Automated Verification of Critical Systems - AVoCS'04, London, Electronic Notes in Computer Science (September 2004).