Axiomatisation of an Interval Calculus for Theorem Proving

We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.

Pockets of flexibility in workflow specification

Workflow technology is currently being deployed in quite diverse domains. However, the element of change is present in some degree and form in almost all domains. A workflow implementation that does not support the process of change will not benefit the organization in the long run. Change can be manifested in different forms in workflow processes. In this paper, we first present a categorization of workflow change characteristics and divide workflow processes into dynamic, adaptive and flexible processes. We define flexibility as the ability of the workflow process to execute on the basis of a loosely, or partially specified model, where the full specification of the model is made at runtime, and may be unique to each instance. To provide a modeling framework that offers true flexibility, we need to consider the factors, which influence the paths of (unique) instances together with the process definition. We advocate an approach that aims at making the process of change part of the workflow process itself. We introduce the notion of an open instance that consists of a core process and several pockets of flexibility, and present a framework based on this notion, which makes use of special build activities that provide the functionality to integrate the process of defining a change, into the open workflow instance.