Automatic verification of concurrent systems using a formula-based compositional approach

摘要

When verifying concurrent systems, described by transition sys- tems, state explosion is one of the most serious problems: systems are often described by transition systems with a prohibitive number of states. The primary cause of this problem is the parallel composition on interacting processes. In the recent years, compositional techniques have been devel- oped to attack the state explosion problem. These techniques are based on dividing the verification task into simpler tasks, exploiting the natural de- composition of complex systems into processes.