Efficient application of symbolic tools for resource booking problems

This paper describes how symbolic model checking tools, like binary decision diagrams (BDDs), may be used to analyze and synthesize supervisors for discrete event systems. As an application, a general routing resource booking problem is considered. A specification language is presented which makes it easy to handle both multiple and alternative resource booking problems. The language is directly translated to a relational model, which is immediately implemented as a BDD. Two optimization concepts, namely smoothing and variable reduction in the BDD representation, are shown to be extremely valuable in handling huge state space problems in a short time