INTERVAL LOGICS AND THEIR DECISION PROCEDURES .2. A REAL-TIME INTERVAL LOGIC

In a companion paper, we presented an interval logic, and showed that it is elementarily decidable. In this paper we extend the logic to all ow reasoning about real-time properties of concurrent systems; we call this logic real-time future interval logic (RTFIL). We model time by the real numbers, and allow our syntax to state the bounds on the dura tion of an interval. RTFIL possesses the ''real-time interpolation pro perty,'' which appears to be the natural quantitative counterpart of i nvariance under finite stuttering. As the main result of this paper, w e show that RTFIL is decidable; the decision algorithm is slightly mor e expensive than for the untimed logic. Our decidability proof is base d on the reduction of the satisfiability problem for the logic to the emptiness problem for timed Buchi automata. The latter problem was sho wn decidable by Alur and Dill in a landmark paper, in which this real- time extension of omega-automata was introduced. Finally, we consider an extension of the logic that allows intervals to be constructed by m eans of ''real-time offsets'', and show that even this simple extensio n renders the logic highly undecidable.