tailieunhanh - CONCUR 2004 – Concurrency Theory- P13

CONCUR 2004 – Concurrency Theory- P13: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | 346 P. Krcal et al. 61 62 63 . are labels on the consumption transitions in the order in which they occur on the path are their absolute timestamps respectively and t eN o for all i. The e-digitalized timed language 7 Ata over alphabet S according to the e-semantics is the set of all e-digitalized timed traces f in Se for Ata- We shall see in the following subsection that for e 1 each run of Ata can have several corresponding e-digitalized timed traces in which the distance between the real-valued timestamp and corresponding digitalized timestamp for each event is limited by e. For the case when e 1 there is only one such e-digitalized timed trace for each run of Ata- This is a useful property of our notion of digitalization. It means that any sequence of events with timestamps in the standard semantics will be caught by at least one digitalized trace. This enables to formulate the correctness criterion as a language inclusion property. An Alternative Characterization We present an alternative characterization of the e-digitalized timed language for timed automata. This characterization establishes a connection between a timed trace and its e-digitalized versions. In the following we use rounded-up time points ft where t denotes the least integer such that t tj. Definition 5. For a timed trace ti ei t2 e2 t3 63 . an e-rounded-up timed trace f e is a possibly infinite sequence t 1 e1 t2 e2 t3 e3 . such that there exists a sequence k1 k2 k3 . where kt e 0 . e-1 for all i 1 l i M ki and . is a non-decreasing sequence of timestamps. The e-rounded-up timed language L Ata V over alphabet S is the set of all e-rounded-up timed traces j where L Ata - For e 1 all ki are equal to 0 and 1-rounded-up timed trace can be constructed just by rounding-up all timestamps of all timed events. Moreover there is just one 1-rounded-up timed trace fl1 for each timed trace f For example for the timed trace a c 6 a . the 1-rounded-up timed trace is f 1 1 a 5 c 8 b 8 a .