Finite-time accuracy of timed discrete event systems

The explicit consideration of time is nowadays crucial for the specification and the verification of Discrete Event Systems (DESs). The behaviour of a DES is characterized by the set of event sequences it generates, its language. In many applications, the DES language is compared to a given set of observed sequences to evaluate the DES accuracy. In a timed context, however, the language is infinite, making it difficult to define and evaluate an accuracy indicator. To overcome this difficulty, the accuracy of a Time Petri net model with respect to a set of sequences is formulated in this paper, using a sliding finite-time window mechanism. In addition, an algorithm to evaluate the proposed accuracy measure is provided.