Guard extraction for modeling and control of a collaborative assembly station

A transition system represented by guards and actions can be amended by new guards computed in order to satisfy some specification. If the transition system is the result of composing smaller state machines, guard extraction can be used to put the new guards onto the guards the original state machines. Planning and verification can then be performed directly on the system with additional guards. In this paper we discuss the benefits of applying guard extraction as part of the modeling work in a modular control architecture, where reusable resources are composed using specifications. We show with an example from the development of an industrial demonstrator that even if the specification language is limited to invariant propositions, in practice many common safety specifications can be expressed when combined with a notion of which transitions are allowed to be restricted.