Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
CONCUR 2004 – Concurrency Theory- P8: 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. | 196 T. Brazdil et al. succ s z . let D s s î G D be the set of transis. Every distribution a G Disc D sy determines Ha Disc Act x S defined for each a t G Note that the sum s so si . sk t of states such that si5G D and s i 0 f r each 0 i k. For each transition s y p we define the set of . -successors of s by succ s p t G S a t 0 for some a e Act . For each state s we define the set of successors by succ s J. For every s G S tions that leave from a unique distribution Act x S as pa a t 52 s h D s a s t exists because the set D s is finite or countably infinite. A combined transition relation De Q S x Disc ActxS is defined by De s a sG S aG Disc D s . We write s M instead of s G De-Obviously introducing combined transitions does not influence the reachability relation. However a single state can have uncountably many outgoing combined transitions. Therefore the triple S Act De cannot be generally seen as a transition system in the sense of Definition 1. Semantic equivalence of probabilistic processes can be formally captured in many ways. Existing approaches extend the ideas originally developed for non-probabilistic processes and the resulting notions have similar properties as their non-probabilistic counterparts. One consequence of this is that probabilistic extensions of bisimulation-like equivalences play a very important role in this setting. First we introduce some useful notions and notation. For the rest of this section let us fix a transition system 5 S Act D . Let E C Sx S be an equivalence relation. We say that two distributions p v e Disc Act xS are equivalent according to E denoted pEu iff for each a G Act and each equivalence class C G S E we have that a C u a C where p a C seC lAa s - In other words the equivalence E defined on states determines a unique equivalence on distributions that is also denoted by E. Definition 2. LetE be an equivalence on S and let s t G 5x5. We say that s t expands in E iff - for each s p there is t yv such that pEu - for .
