tailieunhanh - CONCUR 2004 – Concurrency Theory- P15

CONCUR 2004 – Concurrency Theory- P15: 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. | 406 J. Leroux and G. Sutre Formally let V Q T a 3 S be an n-dim VASS. The set of configuration Cv of V is Q x Nn and the semantics of each transition te T is given by the transition reachability relation Ry t over Cy defined by g x 7 y t x if q a t q 3 t and x x 5 t We write T for the set of all non empty words t0---tk with ti e T and e denotes the empty word. The set T U e of all words ir over T is denoted by T . Transition displacements and transition reachability relations are naturally extended to words S e 0 5 tt t tt 5 t 72y e Idcv TT t 72y 7r 7 .y t A language over T is any subset L of T . We also extend displacements and reachability relations to languages S L tt tr g L andT y L Uren vOr . Definition . Given a VASS V Q T a 3 5 the one-step reachability relation of V is therelation Ry T shortly written Ry- The global reachability relation of V is therelation Rv T shortly written Ry. Remark that the global reachability relation is the reflexive and transitive closure of the one-step reachability relation. The global reachability relation of a VASS V is also usually called the binary reachability relation of V. A reachability subrelation is any relation R C R . For the reader familiar with transition systems the operational semantics of V can be viewed as the infinite-state transition system Cy 7 y . Consider two locations 7 and g in a VASS word tt G T is called a path fromq to q if either 1 tt e and q q or 2 7r to -tk and satisfies q a to q 0 tk and tt-i a ti for every i G 1 fc -A pathfrom q to q is called a loop onq or shortly a loop. We denote by IIv q q the set of all paths from q to q1 in V. The set CU eQ nv q q of all paths in V is written Ily. Notation. In the following we will simply write R resp. II C instead of Rv resp. Ily Cv when the underlying VASS is unambiguous. We will also sometimes write resp. - instead of R resp. R tt R L R . We will later use the following fact which we leave unproved as it is a well known property of VASS. .