dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems

The differential temporal dynamic logic dTL2 is a logic to specify temporal properties of hybrid systems. It combines differential dynamic logic with temporal logic to reason about the inter-mediate states reached by a hybrid system. The logic dTL2 supports some linear time temporal properties of LTL. It extends differential temporal dynamic logic dTL with nested temporalities. We provide a semantics and a proof system for the logic dTL2, and show its usefulness for nontriv-ial temporal properties of hybrid systems. We take particular care to handle the case of alternating universal dynamic and existential temporal modalities and its dual, solving an open problem for-mulated in previous work