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.
Get full access to this article
View all access options for this article.