Checking linear duration invariants by linear programming

Abstract

In this paper, the problem of verifying a timed automaton for a Duration Calculus formula in the form of linear duration invariants [2] is addressed. We show that by linear programming, a particular class of timed automata including the class of real-time automata as a proper subset, can be checked for linear duration invariants. The so-called realtime regular expressions is introduced to express the real-time behaviour of the timed automata in this class. Using real-time regular expressions, an algorithm based on linear programming is presented for checking an automaton in the class with respect to a linear duration invariant.