Formal Encoding and Verification of Temporal Constraints in Clinical Practice Guidelines

In the last decades, clinical practice guidelines have been formulated in order to help decision making about treating specific diseases and promote standards of care quality. Despite the efforts involved to provide solutions for both specifying and verifying temporal constraints in computerized guidelines, none of them is concerned with directly embedding the theoretic semantics of a formal language as the basis of a guideline formalism in order to easily and directly support the temporal perspective. In such a direction, this paper proposes a formal approach which has been seamlessly embedded into a standards-based verifiable guideline model, named GLM-CDS (GuideLine Model for Clinical Decision Support). Such an approach integrates the theoretic semantics of ontology and rule languages to specify and automatically verify a variety of temporal constraints. Such constraints are formulated according to some time patterns, i.e. task duration, periodicity, deadline, scheduling and time lags, and encoded as axioms/formulae verifiable at run-time during the guideline enactment, in order to detect violations or errors occurred with respect to the temporal perspective. As an example of application of the proposed approach, some temporal constraints have been implemented and integrated in GLM-CDS, according to the time patterns identified.