Independent Dynamics Hybrid Automata
(IDA) describe a new class of hybrid automata that
extends decidable O-minimal automata by further allowing identity resets. We define the conditions
under which reachability is decidable over IDA. These conditions involve the satisfiability of first-order
formulæ that limit the interval of time we need to consider to study reachability. In order to prove the
decidability of reachability we mainly exploit the decidability of the first-order formulæ which define
IDA. IDA are useful in the modeling of biological systems where it is possible to have variables which
continue their flows independently (e.g., external input reactants). We briefly comment on how to
model bacterial chemotaxis using IDA.
