An interval logic for higher-level temporal reasoning

During the last several years, we have explored temporal logic as a framework for specifying and reasoning about concurrent programs, distributed systems, and communications protocols. Previous papers[Schwartz/Melliar-Smith81, 82, Vogt82a,b] report on our efforts using temporal reasoning primitives to express very high-level abstract requirements that a program or system is to satisfy. Based on our experiences with those primitives, we have developed an interval logic more suitable for expressing higher-level temporal properties.