Composing Clinical Activity Guidance for Multimorbidity via Bounded Relational Analysis
摘要
Patients with multiple long-term conditions (LTCs) often face physical-activity recommendations that were authored for single conditions, yet such recommendations quite often conflict. We present a lightweight, design-time methodology to formally compose and analyse LTC-specific physical-activity guidelines for multimorbidity. Each guideline is encoded as a named set of Object Constraint Language (OCL) invariants over a shared Unified Modeling Language (UML) schema capturing weekly activity programmes, environment, and patient safety state. Composition is defined as the conjunction of invariant sets and checked for bounded satisfiability using the USE (UML-based Specification Environment) \(\leftrightarrow \) Kodkod relational pipeline. When satisfiable, the analysis synthesizes concrete, symmetry-reduced weekly programmes; when unsatisfiable, it produces a minimal set of inconsistent guidelines, expressed at the level of named clinical rules, to explain incompatibilities. We instantiate the approach with modules for type 2 diabetes, atrial fibrillation, asthma, and an early post-event recovery policy, and evaluate it on three scenarios: compatible, parameter-sensitive, and intrinsically incompatible. The results demonstrate how relational model finding yields interpretable artifacts—satisfiability frontiers, minimal contradiction sets, and concrete programme exemplars—that are auditable by clinicians and exportable as explainable test cases for health decision support.