Signed interval logic. (English) Zbl 0942.03027
Flum, Jörg (ed.) et al., Computer science logic. 13th international workshop, CSL ’99. 8th annual conference of the EACSL, Madrid, Spain, September 20-25, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1683, 157-171 (1999).
Summary: Signed Interval Logic (SIL) is an extension of Interval Temporal Logic (ITL) with the introductin of the notion of a direction of an interval.
We develop syntax, semantics, and proof system of SIL, and show that this proof system is sound and complete. The proof system of SIL is not more complicated than that of ITL but SIL is (contrary to ITL) capable of specifying liveness properties. Other interval logics capable of this (such as Neighbourhood Logic) have more complicated proof systems. We discuss how to define future intervals in SIL for the specification of liveness properties.
To characterize the expressive power of SIL we relate SIL to arrow logic and relational algebra.
For the entire collection see [Zbl 0929.00039].
We develop syntax, semantics, and proof system of SIL, and show that this proof system is sound and complete. The proof system of SIL is not more complicated than that of ITL but SIL is (contrary to ITL) capable of specifying liveness properties. Other interval logics capable of this (such as Neighbourhood Logic) have more complicated proof systems. We discuss how to define future intervals in SIL for the specification of liveness properties.
To characterize the expressive power of SIL we relate SIL to arrow logic and relational algebra.
For the entire collection see [Zbl 0929.00039].
