Dr Juliana Bowles – Computing Conflict-free Treatments for Multiple Chronic Illnesses

Modern treatments for patients with more than one chronic condition can be highly precarious, and in many cases, simultaneous treatments for different illnesses can be detrimental to each other and ultimately, the patient. Dr Juliana Bowles at the University of St Andrews believes that this pressing issue can be solved with the help of advanced computational techniques. Her team has explored the ability of such techniques to calculate reliable outcomes within models of complex systems. Their work promises to significantly enhance the ways in which treatments for chronic conditions could be delivered – improving safety and quality of life for patients.

Webs of Interactions

From natural ecosystems to social networks, the characteristics of many systems are driven by complex webs of interactions between different objects and components. To understand how they work, computer scientists can build behavioural models that predict the outcomes of manipulations to the system – all while obeying the laws of physics.

This approach has previously allowed researchers to virtually probe the behaviours of a diverse range of systems. However, the technique faces one clear limitation: when systems become too large, and governed by many different aspects and variables, they can become far too complex for researchers to build accurate models of them.

To overcome the issue, computer scientists sometimes reflect on individual ‘scenarios of execution’ that are possible within complex systems. Instead of modelling the complete behaviour of a system, the concept focusses on computing the outcomes of specific situations, brought about when systems are manipulated in specific ways. However, this approach has experienced pitfalls. Scenarios of execution can be carried out in a number of different ways, ultimately yielding many different, often conflicting outcomes. Consequently, the results gathered in the process remain inconclusive and unreliable.  

Combining Computational Techniques

In their research, Dr Juliana Bowles and her team at the University of St Andrews have explored an improved approach which integrates a variety of so-called formal methods, including constraint solvers and theorem provers.

In particular, ‘satisfiability modulo theory’ (SMT) solvers allow the team to explore the use of arithmetic and add measures to find properties of interest. When formulating a problem as a series of logical constraints, an SMT solver tries to satisfy all the constraints simultaneously, and if there are conflicting elements, it will identify them. A theorem prover can help to generate the constraints needed by the solver by expressing the problem in a simpler, more natural way. ‘In this context we use the theorem prover “Isabelle”,’ says Dr Bowles. ‘This has the added advantage that we can prove the correctness of the formulations directly within the theorem prover.’

Dr Bowles and Dr Marco Caminati, also at the University of St Andrews, developed an approach that explores the benefits of combining theorem provers and SMT solvers to generate outcomes in complex combinations of models. Their approach can ignore any present inconsistencies within the models, and only find scenarios of execution that are free from inconsistencies with each other.

Reaching Conflict-free Outcomes

By exploiting the advantages of combining Isabelle and SMT solvers, the team revealed that conflict-free outcomes of different scenarios of execution can be computed automatically. They also developed new ways to prove that their calculated results were correct and showed that their methods were more effective than when using solvers alone. To reduce complexity, Dr Bowles and Dr Caminati considered how some constraints of behavioural models can be ranked over others if they are more significant, for instance if treatment of one disease, such as cancer, is prioritised above other comorbidities. They added further flexibility by allowing executions of different scenarios to start at different times.

Ultimately, the duo’s results paved the way for further studies regarding one of the most intricate systems known to science: the human body. In cases of illnesses enduring a lifetime, the body’s responses to highly complex treatment guidelines can be highly unpredictable. Dr Bowles and Dr Caminati realised that these inherent uncertainties have many similarities with the issues they had recently overcome.

‘Although software system specification and patient care guidelines seem different, inherently they have something in common,’ explains Dr Bowles. ‘In both cases we have procedures and executions of (partially) ordered sequences of actions, called “traces of execution” in computer science or “pathways” in clinical practice. In the case of computer-based systems, actions are carried out by users or computers, while in the case of care guidelines, actions are carried out by physicians, patients and carers. In both cases, conflict may arise when individual executions and pathways are incompatible.’

Inconsistencies Between Treatments

The list of conditions that many people globally must endure for their entire lives is unfortunately long, including diabetes, heart and liver diseases, COPD and cancers. To ensure that patients suffering from these diseases have the highest possible lifespans and quality of life, clinicians have now developed treatment regimens incorporating factors including drugs, diet and lifestyle, which they recommend patients should strictly adhere to. So far, such efforts have reduced the suffering of many millions of people worldwide.

The evident problem with this approach is that some patients are likely to suffer from multiple, unrelated chronic conditions at the same time. Since patients dealing with these cases of ‘multimorbidity’ must be treated by multiple doctors, each specialised in just one of their conditions, they will inevitably receive multiple, often conflicting treatment guidelines at the same time.

Because these guidelines are so strict, it becomes highly likely that they will be detrimental to each other – forcing doctors to adapt their treatments to account for other conditions which they likely have little knowledge of. Ultimately, this means that the safety and wellbeing of patients already in challenging situations is at risk. According to Dr Bowles, this demands an urgent rethink in how computer science can further develop automated solutions aimed at improving the approach to treatment of multimorbidity.

Expanding Computational Capabilities

In a further 2019 study, Dr Bowles and her colleagues explored how their computational techniques could be used to significantly streamline our current treatments of multimorbidity. ‘We investigated automated methods of detection of conflicts in clinical pathways for multimorbidities and proposed solutions that resolve them,’ she explains.

Building on results from Dr Bowles’ previous study, the team presented their automated approach with clinical guidelines for specific treatments for chronic conditions. These instructions came in the form of treatment models. When translated into a form a computer could understand, the researchers’ techniques were used to carry out scenarios of execution corresponding to a patient being treated with specific guidelines.

If two or more disease treatment models were fed into the framework, the SMT solver checked for any inconsistencies between them, indicating that one treatment was lowering the effectiveness of another. Subsequently, the correctness of the outcomes of the operation was checked by the automated theorem prover ‘Isabelle’, allowing either positive or negative scores to be assigned to each aspect of each clinical guideline. If any aspects were low or negatively scoring, the researchers could conclude that they were incompatible with other treatments and would need to be adapted.

Reaching the Best Compromise

For the first time, Dr Bowles’ team had demonstrated a computational framework that could identify cases in which multiple clinical guidelines caused problems when carried out at the same time. ‘We have shown how an automated framework combining efficient and formal verification techniques can be used to identify steps in different medical guidelines that cause problems if carried out together, and find the preferred alternative according to certain criteria, such as drug efficacy, prevalent disease, patient allergies,’ she says.

Importantly, the software was able to consider factors including the interactions between two drugs, prescribed for different conditions; between foods and particular drugs; and contradictory health recommendations, including patterns of sleep and exercise. It also accounted for criteria unrelated to treatment, including patient allergies.

Through the scoring system established by the team’s approach, doctors could be given clear guidelines as to the particular aspects of their treatments they need to adapt and aid them in finding a compromise treatment that would be more effective overall. With the success of this approach, Dr Bowles and her colleagues focussed on establishing greater flexibility in the computational framework, which will prove critical if the technique is to be integrated into practical treatments.

Establishing Guideline Flexibility

In reality, patients with multimorbidity will not only be concerned with the overall effectiveness of their multiple treatments; if their quality of life is to improve, a wide variety of other factors must also be considered. With this in mind, Dr Bowles and Dr Caminati have extended the capabilities of their technique further in their latest study. This time, they aimed to go beyond the consideration of medication effectiveness alone as their criteria for the best solution – checking for factors including the different stages of patients’ conditions, and whether certain combinations of treatments were safe and comfortable for them.

If this is not the case, the software is now able to pick the best alternative from a group of potential medications. Furthermore, this list can be tailored to the personal preferences of the patient, including the avoidance of certain side-effects, while also accounting for the timing and dosage of the medication. If these conditions are not satisfied, the software can reverse its previous choices and go back to past decision points, enabling it to find solutions better suited to any pre-determined criteria.

Hope for Better Guidelines

The research of Dr Bowles, Dr Caminati and their colleagues is timely; multimorbidity is now a growing problem worldwide, with over half of people with chronic conditions in Scotland alone suffering from an additional comorbidity. Yet through the combination of SMT solvers with ‘Isabelle’, the team’s software offers flexible solutions to the treatment requirements of a diverse range of patients. With this infrastructure in place, the researchers’ techniques could now easily be adapted to account for other factors, including costs, the number of medications prescribed, and even biomarkers for targeted treatments, provided this information is known and available.

Through further research, Dr Bowles hopes to integrate the techniques into real clinical decision support systems, which will enable doctors to tailor their treatments both to the needs of their patients, and to the treatment guidelines of other conditions that they know less about. Her work now holds the promise to enable patients with incurable diseases to live more comfortable lives despite their conditions, with the peace of mind that the treatments they are receiving are optimised and that harmful side-effects and interactions are minimised.