br0050 Eugene Asarin, Nicolas Basset, Aldric Degorre, Spectral gap in timed automata, in: Lect.br0040 Eugene Asarin, Nicolas Basset, Marie-Pierre Béal, Aldric Degorre, Dominique Perrin, Toward a timed theory of channel coding, in: Lect.Dill, Model-checking for probabilistic real-time systems (extended abstract), in: Lect. br0020 Rajeev Alur, Costas Courcoubetis, David L.Cover, A sandwich proof of the Shannon-McMillan-Breiman theorem, Ann. We also show that Y * enjoys well known properties in ergodic and information theory, namely, Y * is ergodic and satisfies an asymptotic equipartition property. The formula defining Y * is an adaptation of the so-called Shannon-Parry measure to the timed automata setting. 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). This ensures that, among the stochastic process over runs of a given TA, Y * is the one that permits to sample runs of the TA in the most uniform way possible. Our main contribution is an explicit formula defining a process Y * which maximizes the entropy. We adapt the notion of Shannon (continuous) entropy to such processes. 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 give an answer to this question using a maximal entropy approach. 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. Several ways of assigning probabilities to runs of timed automata (TA) have been proposed recently.
0 kommentar(er)
