Linear duration invariants

Abstract

This paper is to present an algorithm to decide whether a real-time system satisfies a set of invariants which are constructed from linear inequalities of integrated durations of system states. Real-time systems in the paper are taken to be real-time automata which set up for each of state transitions a lower time bound and an upper time bound. The satisfaction problem can be translated into a family of linear programming problems. The algorithm is, according to the invariants, to reduce the infinite family of linear programming problems to an equivalent one with only finite members, and then to solve each of linear programming problems efficiently. The algorithm is so simple that no prerequisite of linear programming theory is assumed.