Title: Compositional verification and specification of refinement for reactive systems in a dense time temporal logic