Automatic Abstraction of Synchronization Sequences
Sven Bünte
The exponential state-space blow-up that arises when analyzing reachability in networks of synchronizing processes is one of the main problems in model checking. This thesis will introduce an approach in which communication sequences are abstracted algebraically. The abstraction includes information about safety properties in such a way that if the solution set of the abstraction is empty, the stated properties hold. All involved means have at most polynomial complexity. Since the solution space is an overapproximation, the checking procedure is incomplete yet. However, the ideas and methods that will be introduced form a nice basis for doing further abstraction refinement such that valuable information about reachability might be derived conveniently in the future.
Bachelor Thesis.