Performance Measured by Timed Automata
Timed automata as a specification formalism for stochastic systems
Jan Krcal, Faculty of Informatics Masaryk University, Brno, Czech Republic
- Date and Time
Wednesday, October 27th, 2010 at 10:30
Polacksbacken, room 1213
Continuous-time stochastic processes model systems containing both real time and randomness. In the talk I explain a general concept of using a timed automaton as an observer of a stochastic process (such as continuous-time Markov chain). All the non-determinism of the timed automaton is resolved by the stochastic process.
- First, we may use the observer to express a linear-time property. In such case we ask, what is the probability that in the stochastic process this property is satisfied.
- Second, using the observer we may study the long-run average properties of the stochastic process (e.g. what percentage of time a linear-time property is satisfied).