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

Mar 18, 2020 | Editor's Pick, Engineering & Computer Science, Medical & Health Sciences

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.


Meet the researcher

Dr Juliana Bowles

School of Computer Science
University of St Andrews
St Andrews
United Kingdom

Dr Juliana Bowles was awarded her PhD at the Technical University Braunschweig, Germany, in 2000. After working as a postdoctoral researcher at the University of Edinburgh, she then took a lectureship position at the University of Birmingham in 2004. In 2007, Dr Bowles moved to the University of St Andrews in Scotland, where she is currently a Senior Lecturer in the School of Computer Science. Dr Bowles’ research interests lie in the development of automated techniques for computer modelling, especially in healthcare. She is particularly dedicated to using computational methods to maximise safety and medication effectiveness for patients undergoing multiple treatments. She has presented her team’s findings at several international conferences, in addition to events with the general public and GPs, which has generated considerable international interest. She also leads the EU Horizon 2020 research project SERUMS, which deals with the security and privacy of future-generation healthcare systems, putting patients at the centre of future healthcare provision, enhancing their personal care and maximising the quality of treatment they receive.


E: jkfb@st-andrews.ac.uk

W: https://hig.cs.st-andrews.ac.uk/people/staff/juliana-bowles/


Dr Marco Caminati, University of St Andrews


EU Horizon 2020





J Bowles, MB Caminati, Correct composition in the presence of behavioural conflicts and dephasing. Science of Computer Programming, 2020, 185, 102323.

J Bowles, MB Caminati, An integrated approach to a combinatorial optimisation problem, In: Ahrendt W., Tapia Tarifa S. (eds) Integrated Formal Methods, IFM 2019, Lecture Notes in Computer Science, 2019, vol. 11918, pp 284-302.

J Bowles, MB Caminati, S Cha, J Mendoza, A framework for automated conflict detection and resolution in medical guidelines, Science of Computer Programming, 2019, 182, 42-63.

J Bowles, MB Caminati, Balancing Prescriptions with Constraint Solvers, In Automated Reasoning for Systems Biology and Medicine, 2019, 30, 243-267.

Creative Commons Licence
(CC BY 4.0)

This work is licensed under a Creative Commons Attribution 4.0 International License. Creative Commons License

What does this mean?

Share: You can copy and redistribute the material in any medium or format

Adapt: You can change, and build upon the material for any purpose, even commercially.

Credit: You must give appropriate credit, provide a link to the license, and indicate if changes were made.

More articles you may like

Professor Aaron Brown | Brown Adipose Tissue and Optogenetics – The Next Step in Obesity Treatment?

Professor Aaron Brown | Brown Adipose Tissue and Optogenetics – The Next Step in Obesity Treatment?

Adipose tissue is more commonly known as body fat. Unlike white adipose tissue, which is linked to negative cardiovascular outcomes such as metabolic syndrome, brown adipose tissue is positively related to health and may reduce the risk of cardiometabolic diseases. Professor Aaron Brown and his team at the MaineHealth Institute for Research are working to understand brown adipose tissue regulation and explore its therapeutic potential. They have already made significant advancements through the application of optogenetics, a cutting-edge technique that harnesses the power of light to precisely manipulate specific cellular processes.

Dr Kimberly Kay Hoang | Who Gets to Be a Theorist? The Oppression of Marginal Theories

Dr Kimberly Kay Hoang | Who Gets to Be a Theorist? The Oppression of Marginal Theories

Who gets to be a theorist? What kinds of theoretical work get marginalised in academic research? And how does this oppression play out in the peer-review process? Dr Kimberly Kay Hoang is a Professor of Sociology at the University of Chicago. She has explored how difficult it is to get your sociology research published if you are not using research deemed to be legitimate by reviewers. She brings awareness to these issues and argues for change amongst scholars so that new forms of knowledge are not missed, especially regarding feminist, minority and racial theories.

Dr Kimberly Kay Hoang | Spiderweb Capitalism: The Secret Financial Webs Built by the Ultra-Wealthy

Dr Kimberly Kay Hoang | Spiderweb Capitalism: The Secret Financial Webs Built by the Ultra-Wealthy

The anonymous leak of the Panama Papers in 2016 revealed how the exceptionally wealthy (such as politicians, celebrities and business leaders) hide their money and exploit secretive offshore tax regimes. Dr Kimberly Kay Hoang is a Professor of Sociology at the University of Chicago, and after six years of research, hundreds of interviews and travelling 350,000 miles, she published Spiderweb Capitalism: How Global Elites Exploit Frontier Markets. She uncovered the mechanisms behind the movement of money into and out of Southeast Asia, and how that money travels all over the world.

Dr Ian Maxwell | Patents, Politics and Products: Considering Chinese-Owned Australian Patents

Dr Ian Maxwell | Patents, Politics and Products: Considering Chinese-Owned Australian Patents

Patents, or holding the intellectual property rights to an invention, can be of great importance to a company, as they allow them to sell their product in a specific market with reduced competition. Dr Ian Maxwell has recently considered the patents filed by Chinese entities in Australia, looking in particular at the recent growth in the number of these patents being filed. He considers the interplay between patents and political rulings and provides several insightful statistics about these Chinese-owned Australian patents.