Relating time progress and deadlines in hybrid systems
Time progress conditions in hybrid systems are usually specified in terms of invariants, predicates characterizing states where time can continuously progress, or in terms of deadline conditions, predicates characterizing states where time progress immediately stops. These specifications are each other's duals. The aim of this work is the study of relationships between general time progress conditions and these generated by using state predicates. It is shown that using deadline conditions or invariants allows to characterize all practically interesting time progress conditions. The study is performed by using a Galois connection between the corresponding lattices. We provide conditions for the connection to be a homomorphism and apply the results to the compositional description of hybrid systems
HART97.pdf
openaccess
1.88 MB
Adobe PDF
12a46ab0a8e549e1d9b90f4b7099dcab