Process decomposition via synchronization events and its application to counter-process decomposition

摘要

In this paper, we consider a process decomposition problem which allows one to use additional synchronization events, and propose a new decomposition method. The process decomposition problem is such that given a single labeled transition system (LTS) L{sub}(in), construct LTSs L{sub}1, . . .,L{sub}n such that the composite process of L{sub}1,..., L{sub}n is observably bisimulation equivalent to L{sub}(in). The main advantage of the proposed method is that the size of the decomposed LTSs is often much smaller than known methods. Especially, we focus on simple counters and generalized counters and present an algorithm which decomposes a simple (or generalized) counter into smaller counters by using the proposed method.