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. This question does not seem to have been studied yet. We give an answer to it using a maximal entropy approach. We introduce our variant of 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 * which maximizes the entropy. This formula is an adaptation of the so-called Shannon-Parry measure to the timed automata setting. The process Y * has the nice property to be ergodic. As a consequence it has the asymptotic equipartition property and thus the random sampling w.r.t. Y * is quasi uniform.
KeywordsProbability Density Function Model Check Maximal Entropy Strong Connectivity Time Automaton
Unable to display preview. Download preview PDF.
- 3.Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for probabilistic real-time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, Springer, Heidelberg (1991)Google Scholar
- 11.Bertrand, N., Bouyer, P., Brihaye, T., Markey, N.: Quantitative model-checking of one-clock timed automata under probabilistic semantics. In: QEST, pp. 55–64. IEEE Computer Society (2008)Google Scholar
- 12.Billingsley, P.: Probability and measure, vol. 939. Wiley (2012)Google Scholar
- 13.Bouyer, P., Brihaye, T., Jurdziński, M., Menet, Q.: Almost-sure model-checking of reactive timed automata. QEST 2012, 138–147 (2012)Google Scholar
- 14.Cover, T.M., Thomas, J.A.: Elements of information theory, 2nd edn. Wiley (2006)Google Scholar
- 18.Lind, D., Marcus, B.: An Introduction to Symbolic Dynamics and Coding. Cambridge University Press (1995)Google Scholar
- 20.Parry, W.: Intrinsic Markov chains. Transactions of the American Mathematical Society, 55–66 (1964)Google Scholar
- 21.Shannon, C.E.: A mathematical theory of communication. Bell Sys. Tech. J. 27, 379–423, 623–656 (1948)Google Scholar