A REAL-TIME INTERVAL LOGIC AND ITS DECISION PROCEDURE

Real-Time Future Interval Logic is a temporal logic in which formulae have a natural graphical representation, resembling timing diagrams. I t is a dense real-time logic that is based on two simple temporal prim itives: interval modalities for the purely qualitative part and durati on predicates for the quantitative part. This paper describes the logi c and gives a decision procedure for satisfiability by reduction to th e emptiness problem for Timed Buchi Automata. This decision procedure forms the core of an automated proof-checker for the logic. The logic does not admit instantaneous states, and is invariant under real-time stuttering, properties that facilitate proof methods based on abstract ion and refinement. The logic appears to be as strong as one can hope for without sacrificing elementary decidability. Two natural extension s of the logic, along lines suggested in the literature, lead to eithe r non-elementariness or undecidability.