Monitoring hybrid process specifications with conflict management: An automata-theoretic approach

Complexity of medical treatments can vary from prescribing medicine for a specific ailment to managing a complex set of simultaneous medical issues. In the latter case, doctors are assisted by clinical guidelines which outline standard medical procedures, tests, treatments, etc. To facilitate the use of such guidelines, they can be digitized as processes and adopted in complex process engines offering additional help to health providers such as decision support while monitoring active treatments so as to detect flaws in treatment procedures and suggest possible reactions on them. For example, a patient may present symptoms of multiple diseases simultaneously (requiring multiple clinical guidelines to be followed), while also being allergic to some often-used drugs (requiring additional constraints to be respected). This can easily lead to treating a patient based on a set of process specifications which are not fully compatible with each other. While a scenario like that commonly occurs in practice, research in that direction has thus far given little consideration to how to specify multiple clinical guidelines and how to automatically combine their specifications in the context of the monitoring task. In our previous work (Alman et al., 20222), we presented a conceptual framework for handling the above cases in the context of monitoring. In this paper, we present the algorithms necessary for implementing key components of this conceptual framework. More specifically, we provide formal languages for representing clinical guideline specifications and formalize a solution for monitoring the interplay of such specifications expressed as a combination of (data-aware) Petri nets and temporal logic rules. The proposed solution seamlessly handles combination of the input process specifications and provides both early conflict detection and decision support during process execution. We also discuss a proof-of-concept implementation of our approach and present the results of extensive scalability experiments.