A logic for signal inserted timed frames

Abstract

We propose a first-order predicate logic TFL of timed frames extended with signals. This logic combines a simple syntax with a high expressivity; it can distinguish frames that are not the same as sets of transitions and states. We show how Dicky logic and CTL can be embedded in TFL.