Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings
Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings
复制标题
综合形式方法 - 第 15 届国际会议，IFM 2019，挪威卑尔根，2019 年 12 月 2-6 日，会议记录
DOI：
10.1007/978-3-030-34968-4_16
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Bowles J
中科院分区：
文献类型：
--
作者：
Bowles J
我们从医疗保健领域的一个问题中汲取灵感，其中患有多种慢性疾病的患者遵循针对个体疾病设计的不同指南，其目的是为患者找到避免药物不良反应的最佳治疗计划，尊重患者的偏好并优先考虑药物疗效。每个慢性病症指南可以由有向图抽象地描述，其中每个节点指示治疗步骤（例如，药物或资源的选择）并且具有一定的持续时间。最佳治疗路径的搜索被看作是一个组合优化问题，我们展示了如何选择一个路径，通过资源兼容性的概念约束的图形。这个概念考虑了任何有限数量的资源之间的相互作用，并使得表达非单调的相互作用成为可能。我们的形式化还引入了一个离散的时间度量，以便在优化过程中只考虑同时节点。我们表示的形式问题作为SMT问题，并提供了一个正确的证明SMT代码之间的相互作用，利用SMT求解器和证明助理伊莎贝尔/HOL。我们考虑的问题结合了最优图执行和资源分配方面，显示了SMT求解器如何成为在相应领域中得到充分研究的其他方法的替代方案。
We take inspiration from a problem from the healthcare domain, where patients with several chronic conditions follow different guidelines designed for the individual conditions, and where the aim is to find the best treatment plan for a patient that avoids adverse drug reactions, respects patient’s preferences and prioritises drug efficacy. Each chronic condition guideline can be abstractly described by a directed graph, where each node indicates a treatment step (e.g., a choice in medications or resources) and has a certain duration. The search for the best treatment path is seen as a combinatorial optimisation problem and we show how to select a path across the graphs constrained by a notion of resource compatibility. This notion takes into account interactions between any finite number of resources, and makes it possible to express non-monotonic interactions. Our formalisation also introduces a discrete temporal metric, so as to consider only simultaneous nodes in the optimisation process. We express the formal problem as an SMT problem and provide a correctness proof of the SMT code by exploiting the interplay between SMT solvers and the proof assistant Isabelle/HOL. The problem we consider combines aspects of optimal graph execution and resource allocation, showing how an SMT solver can be an alternative to other approaches which are well-researched in the corresponding domains.