Although the set of reachable states of a lossy channel system (LCS) is regular, it is well-known that this set cannot be constructed effectively. In this paper, we characterize significant classes of LCS for which the set of reachable states can be computed. Furthermore, we show that, for slight generatlizations of these classes, computability can no longer be achieved. To carry out our study, we define rewriting systems which capture the behaviour of LCS, in the sense that (i) they have a FIFO-like semantics and (ii) their languages are downward closed with respect to the substring relation. The main result of the paper shows that, for context-free rewriting systems, the corresponding language can be computed. An interesting consequence of our results is that we get a characterization of classes of meta-transitions whose post-images can be effectively constructed. These meta-transitions consist of sets of nested loops in the control graph of the system, in contrast to previous works on meta-transitions in which only single loops are considered. Essentially the same proof technique we use to show the result mentioned above allows also to establish a result in the theory of OL-systems, i.e., context-free parallel rewriting systems. We prove that the downward closure of the language generated by any OL-system is effectively regular.
展开▼
