Construction process modeling: Representing activities, items and their interplay

General purpose process modeling approaches are meant to be applicable to a wide range of domains. To achieve this result, their constructs need to be general, thus failing in capturing the peculiarities of a particular application domain. One aspect usually neglected is the representation of the items on which activities are to be executed. As a consequence, the model is an approximation of the real process, limiting its reliability and usefulness in particular domains. We extend and formalize an existing declarative specification for process modeling mainly conceived for the construction domain. In our approach we model the activities and the items on which the activities are performed, and consider both of them in the specification of the flow of execution. We provide a formal semantics in terms of LTL over finite traces which 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.