Department of Computer Science

Permanent URI for this community

Now showing 1 - 1 of 1

Reducing the state explosion problem during model checking
(Stellenbosch : Stellenbosch University, 1991-03) Barnard, Dieter Cornelius; De Villiers, P. J. A.; Krzesinkski, A. E.; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Computer Science.
ENGLISH ABSTRACT: Our Department is currently engaged in a project to verify concurrent systems. The project is based on the model checking verification technique and a model checker was implemented using transition systems as a modelling language and computation tree logic (CTL) as a specification language. This technique has one serious limitation: the model checker has to generate the reachable state space of a transition system and this state space can be very large. An unmanageable reachable state space is known as a state explosion, and could prohibit the use of model checking for practical concurrent systems. This thesis investigates the state explosion problem encountered during the model checking of transition systems. A survey of solutions to the state explosion problem is presented from which model reduction is chosen for implementation. Because no reduction methods have been developed for transition systems, a suitable Petri net reduction technique is adapted for the reduction of transition systems. The technique is implemented and proved to correctly reduce a transition system. A summary of performance of the reduction technique is provided.