CoPModL: Construction Process Modeling Language and Satisfiability Checking

Process modeling has been widely investigated in the literature and several general purpose approaches have been introduced, addressing a variety of domains. However, generality goes to the detriment of the possibility to model details and peculiarities of a particular application domain. As acknowledged by the literature, known approaches predominantly focus on one aspect between control flow and data, thus neglecting the interplay between the two. Moreover, process instances are not considered or considered in isolation, neglecting, among other aspects, synchronization points among them. As a consequence, the model is an approximation of the real process, limiting its reliability and usefulness in particular domains. This observation emerged clearly in the context of a research project in the construction domain, where preliminary attempts to model inter-company processes show the lack of an appropriate language. Building on a semi-formal language tested on real construction projects, in this paper we define CoPModL, a process modeling language which accounts both for activities and items on which activities are to be executed. The language supports the specification of different item-based dependencies among the activities, thus serving as a synchronization specification among several activity instances. We provide a formal semantics for the language in terms of LTL over finite traces. This paves the way for the development of automatic reasoning. In this respect, we investigate process model satisfiability and develop an effective algorithm to check it. (c) 2019 Elsevier Ltd. All rights reserved.