Department of Information Technology

Abstract 2007-02-01

Pavel Krcal

Timed automata received recognition because of their simplicity and ease
with which they handle real time. Adding real valued clocks to the finite
automata significantly increased the modeling power while many properties of
the new model remained as nice as in the discrete case. In spite of their
general acceptance, timed automata also brought many questions and problems,
mostly caused by the fact that the clocks run and can be measured with the
infinite precision.

Standard analysis methods for timed automata are based on simple comparisons
of the clock values. However, this method is not sufficient in many
cases. Clock difference relations (CDRs) are structures which allow us to
compare clock differences. We present CDRs and several problems which
require such a refined information for their solution. We will discuss
notions of Zenoness, implementability, or reasonable strategies for timed
games on the semantical level and present two problems related to
desynchronization of timed automata.

Updated  2007-01-29 11:58:17 by Sven Sandberg.