Department of Information Technology

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).

Back to the seminar page

Updated  2010-10-25 12:34:33 by Frédéric Haziza.