A grounding of business process modeling based on temporal logic

This paper proposes grounding for the business process modeling (BPM) based on general time theory providing axiomatic system. First order logic is used to give a clear definition of abstract business process and corresponding temporal relations including derived relations using a single “Meets” relation. Temporal logic used here treats time interval and time points on equal footing. We use model theoretic approach, in which abstract business process is represented as a formal system and mapped to an instance/concrete realization. Also, we used resolution theorem to provide its soundness and completeness properties. A Process temporal graph as a directed graph is introduced with graphical notation defined to represent the temporal knowledge. A real world realization of the corresponding graph is considered an instance of an abstract business process. Sound and completeness properties of the process temporal graph using reachability analysis. However, Arcs representing time elements, vertex representing the `Meets´ relation and also allows expression of both logical AND and OR.