Real-time Specification and Reasoning Using Maximal Intervals

摘要

Interval-based formalisms for real-time systems describe behaviour via the time intervals during which predicates on the system state hold. However, these formalisms are clumsy for relating the occurrences of state changes, or events. Here we overcome this by introducing definitions and laws for maximal intervals. These define the longest time intervals over which a predicate holds, and their endpoints thus mark significant state changes.