\input zb-basic
\input zb-ioport
\iteman{io-port 00984745}
\itemau{Ramakrishna, Y.S.; Melliar-Smith, P.M.; Moser, L.E.; Dillon, L.K.; Kutty, G.}
\itemti{Interval logics and their decision procedures. II: A real-time interval logic.}
\itemso{Theor. Comput. Sci. 170, No.1-2, 1-46 (1996).}
\itemab
Summary: In Part I [ibid. 166, 1-47 (1996; Zbl 0872.03019)], we presented an interval logic, and showed that it is elementarily decidable. We extend the logic to allow 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 duration of an interval. RTFIL possesses the ``real-time interpolation property,'' which appears to be the natural quantitative counterpart of invariance under finite stuttering. As the main result of this paper, we show that RTFIL is decidable; the decision algorithm is slightly more expensive than for the untimed logic. Our decidability proof is based on the reduction of the satisfiability problem for the logic to the emptiness problem for timed B\"uchi automata. The latter problem was shown 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 means of ``real-time offsets'', and show that even this simple extension renders the logic highly undecidable.
\itemrv{~}
\itemcc{}
\itemut{reasoning about real-time properties of concurrent systems; real-time future interval logic; decision algorithm; decidability; satisfiability problem; timed B\"uchi automata}
\itemli{doi:10.1016/S0304-3975(96)80701-8}
\end