AXIOMATIZATIONS OF INTERVAL LOGICS

Article type: Research Article

Authors: Kutty, G. | Moser, L.E. | Melliar-Smith, P.M. | Ramakrishna, Y.S. | Dillon, L.K.

Affiliations: Department of Electrical and Computer Engineering, Department of Computer Science, University of California, Santa Barbara 93106

Abstract: Interval logic has been introduced as a temporal logic that provides higher-level constructs and an intuitive graphical representation, making it easier in interval logic than in other temporal logics to specify and reason about concurrency in software and hardware designs. In this paper we present axiomatizations for two propositional interval logics and relate these logics to Until Temporal Logic. All of these logics are discrete linear-time temporal logics with no next operator. The next operator obstructs the use of hierarchical abstraction and refinement, and makes reasoning about concurrency difficult.

DOI: 10.3233/FI-1995-2441

Journal: Fundamenta Informaticae, vol. 24, no. 4, pp. 313-331, 1995