A maximal entropy stochastic process for a timed automaton

Several ways of assigning probabilities to runs of timed automata (TA) have been proposed recently. When only the TA is given, a relevant question is to design a probability distribution which represents in the best possible way the runs of the TA. We give an answer to this question using a maximal entropy approach. We introduce our variant of a stochastic model, the stochastic process over runs, which permits to simulate random runs of any given length with a linear number of atomic operations. We adapt the notion of Shannon (continuous) entropy to such processes. Our main contribution is an explicit formula defining a process Y⁎Y⁎ which maximizes the entropy. This ensures that, among the stochastic process over runs of a given TA, Y⁎Y⁎ is the one that permits to sample runs of the TA in the most uniform way possible. Hence, our method could be used in a statistical model checking framework, providing a non-trivial yet natural way to generate runs in a quasi-uniform manner (described in the article). The formula defining Y⁎Y⁎ is an adaptation of the so-called Shannon–Parry measure to the timed automata setting. We also show that Y⁎Y⁎ enjoys well known properties in ergodic and information theory, namely, Y⁎Y⁎ is ergodic and satisfies an asymptotic equipartition property.