Tata Institute of Fundamental Research
Observing Markov Chains by Timed Automata
Seminar
Speaker:
Joost-Pieter Katoen
RWTH Aachen University
LS2: Software Modeling and Verification
D-52056 Aachen
Germany
Date:
Friday, 16 Dec 2011, 11:30 to 12:30
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
Markov chains are omnipresent. They are used as semantical backbone of Markovian queueing networks, stochastic Petri nets, stochastic process algebras, and calculi for systems biology. Abundant applications in performance, reliability and dependability analysis use Markov chains. The specification of measures-of-interest is however quite limited, and dedicated algorithms are typically developed for every new measure.
In this talk, we will survey model checking techniques for Markov chains. On the one hand, temporal logics allow to express most measures of interest as well as measures that go beyond the classical one. On the other hand, a single model-checking algorithm suffices to deal with all measures that can be expressed.
We will describe the basic model-checking algorithms, covering both discrete-time and continuous-time Markov chains, and report on recent progress on using timed automata as requirements (rather than temporal logic).
| Speaker: | Joost-Pieter Katoen RWTH Aachen University LS2: Software Modeling and Verification D-52056 Aachen Germany |
| Date: | Friday, 16 Dec 2011, 11:30 to 12:30 |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
Markov chains are omnipresent. They are used as semantical backbone of Markovian queueing networks, stochastic Petri nets, stochastic process algebras, and calculi for systems biology. Abundant applications in performance, reliability and dependability analysis use Markov chains. The specification of measures-of-interest is however quite limited, and dedicated algorithms are typically developed for every new measure.
In this talk, we will survey model checking techniques for Markov chains. On the one hand, temporal logics allow to express most measures of interest as well as measures that go beyond the classical one. On the other hand, a single model-checking algorithm suffices to deal with all measures that can be expressed.
We will describe the basic model-checking algorithms, covering both discrete-time and continuous-time Markov chains, and report on recent progress on using timed automata as requirements (rather than temporal logic).
In this talk, we will survey model checking techniques for Markov chains. On the one hand, temporal logics allow to express most measures of interest as well as measures that go beyond the classical one. On the other hand, a single model-checking algorithm suffices to deal with all measures that can be expressed.
We will describe the basic model-checking algorithms, covering both discrete-time and continuous-time Markov chains, and report on recent progress on using timed automata as requirements (rather than temporal logic).