The behavioral composition of services entails the computation of the asynchronous product of automata. The resulting product is tested for bisimulation equivalence with the requested service. This equivalence testing becomes infeasible when the number of services is large. In this paper we propose a symbolic method, based on OBDD, to make the computation feasible. The efficiency of our solution stems from the fact that, in addition to the inherent efficiency of the OBDD method, the OBDD of the product need not be stored in memory but is computed as a disjunction of the individual terms.
展开▼
