Approximate Model Checking of Real-time Systems for Linear Duration Invariants

Real-time systems are usually modelled with timed automata and real-time requirements relating to the state durations are specifiable using linear duration invariants which is a decidable subclass of duration calculus formulas. Different algorithms were developed to check timed automata or real-time automata for linear duration invariants, each needs complicated preprocessing and exponential calculation. To the best of our knowledge, these algorithms have not been implemented as a tool. In this paper, we present an approximate model checking technique based on genetic algorithm to get information about whether real-time automata satisfy linear duration invariants in reasonable times. Genetic algorithm is a good optimization method when problem needs massive computation, and it particularly works well in our case because fitness function derived from the linear duration invariant is linear.