We address the verification problem of FIFO-channel systems by applying the symbolic analysis principle. We represent their sets of states (configurations) using structures called CQDD's allow forward and backward reachability analysis of systems with nonregular sets of configurations. Moreover, we prove that CQDD's allow to compute the exact effect of the repeated execution of any fixed cycle in the transition graph of a system. We use this fact to define a generic reachability analysis semi-algorithm parametrized by a set of cycles #THETA#. Given a set of configurations, this semi-algorithmperforms a least fixpoint calculation to construct the set of its successors (or predecessors). At each step, this calculation is accelerated by considering the cycles in #THETA# as additional "meta-transitions" in the transition graph, generalizing the approach adopted in [5].
展开▼
