Unternehmen stehen immer größeren Herausforderungen gegenüber, wie z.B. internationaler Konkurrenz durch die Globalisierung und immer kürzere Produktlebenszyklen. Einen Wettbewerbsvorteil gegenüber der Konkurrenz können sich die Unternehmen erarbeiten, die schnell und flexibel auf Marktveränderungen reagieren können. Ein gutes und effizientes Geschäftsprozessmanagement ist ein geeignetes Mittel für Unternehmen, sich diesen wachsenden Herausforderungen zu stellen. Daher gibt es auch immer mehr Tools, mit dem sich Geschäftsprozesse erstellen und ändern lassen, um auf diese Weise die Unternehmen beim Geschäftsprozessmanagement zu unterstützen. In der vorliegenden Arbeit werden Möglichkeiten erarbeitet, um Geschäftsprozesse mit Regeln zu erweitern, die die Arbeit mit Geschäftsprozessen unterstützen. Diese Regeln werden in einer temporalen Logik formuliert und sollen von einem Model Checker überprüft werden können, daher wird in dieser Arbeit auch auf temporale Logiken und Model Checker eingegangen.