VALIDATION OF STOCHASTIC SYSTEMS

Publikum
Vorbesprechung
Anmeldung
Überblick über das Seminar
Dozent
Assistent
Literatur

Publikum

Dieses Seminar richtet sich an Studierende im Master oder Bachelor Informatik. Auf Anfrage koennen evtl. einzelne Plätze als

Proseminar angeboten werden.

 


Vorbesprechung

Die Vorbesprechung findet am 6. Nov um 16:30 im SR 013 (Bldg. 45/E.13) statt


Anmeldung

Wenn Sie an dem Seminar teilnehmen wollen, melden Sie sich bitte in unserem

Course Managment System an. Sie müssen sich eventuell zunächst für ein Student Account anmelden.


Überblick über das Seminar

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.


Dozent

Prof. Dr.-Ing. Holger Hermanns

Assistent

Lijun Zhang

Literatur


  • Zeit-Diskret 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]
  • 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]
  • 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.
  • Model Checking Probabilistic CTL (1)
  • Model Checking Probabilistic CTL (2)
  • Model Checking LTL
  • Model Checking 3-valued Probabilistic CTL
    • M. Leucker, V. Wolf: Don't Know in Probabilistic Systems. 2005.
    • Joost-Pieter Katoen, Martin Leucker, Daniel Klink and Verena Wolf. Three-Valued Abstraction for Continuous-Time Markov Chains
  • Verifikation von Markov Entscheidungsprozessen
  • Model Checking Continuous Stochastic Logic (1)
  • Model Checking Continuous Stochastic Logic (2)
  • Verifikation diskret-kontinuierlicher Markov Ketten mit Kosten
  • Verifikation zeit-kontinuierlicher Markov Ketten mit Kosten (1)
  • Verifikation zeit-kontinuierlicher Markov Ketten mit Kosten (2)
  • Verifikation von cost-extended Markov Entscheidungsprozessen
  • Verifikation zeit-kontinuierlicher Markov Entscheidungsprozesse
  • Coupling and self-stabilization