Skip to main content


Predictability of event occurrences in timed systems


Franck Cassez and Alban Grastien



Australian National University


We address the problem of predicting events’ occurrences in partially observable timed systems modelled by timed automata. Our contribution is many-fold: 1) we give a definition of bounded predictability, namely k-predictability, that takes into account the minimum delay between the prediction and the actual event’s occurrence; 2) we show that 0-predictability is equivalent to the original notion of predictability of S. Genc and S. Lafortune; 3) we provide a necessary and sufficient condition for k-predictability (which is very similar to k-diagnosability) and give a simple algorithm to check k-predictability; 4) we address the problem of predictability of events’ occurrences in timed automata and show that the problem is PSPACE-complete.

BibTeX Entry

    publisher        = {Springer},
    author           = {Cassez, Franck and Grastien, Alban},
    year             = {2013},
    month            = aug,
    editor           = {{Victor A. Braberman and Laurent Fribourg}},
    keywords         = {timed automata, predictability, fault diagnosis},
    title            = {Predictability of Event Occurrences in Timed Systems},
    booktitle        = {11th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS)},
    pages            = {62--76},
    address          = {Buenos Aires, Argentina}


Served by Apache on Linux on seL4.