|
We show the regularity of the discrete time behaviour of hybrid
automata in which the rates of continuous variables are governed by
linear differential operators in a diagonal form and in which the
values of the continuous variables can be observed only with finite
precision. We do not demand resetting of the values of the continuous
variables during mode changes. We can cope with polynomial guards and
we can tolerate bounded delays both in sampling the values of the
continuous variables and in effecting changes in their rates required
by mode switchings. We also show that if the rates are governed by
diagonalizable linear differential operators with rational eigenvalues
and there is no delay in effecting rate changes, the discrete time
behaviour of the hybrid automaton is recursive. However, the control
state reachability problem in this setting is undecidable.
[.pdf]
|