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

Dr Tsun-Kong Sham – Dr Jiatang Chen – Dr Zou Finfrock – Dr Zhiqiang Wang | X-Rays Shine Light on Fuel Cell Catalysts

Dr Tsun-Kong Sham – Dr Jiatang Chen – Dr Zou Finfrock – Dr Zhiqiang Wang | X-Rays Shine Light on Fuel Cell Catalysts

Understanding the electronic behaviour of fuel cell catalysts can be difficult using standard experimental techniques, although this knowledge is critical to their fine-tuning and optimisation. Dr Jiatang Chen at the University of Western Ontario works with colleagues to use the cutting-edge valence-to-core X-ray emission spectroscopy method to determine the precise electronic effects of altering the amounts of platinum and nickel in platinum-nickel catalysts used in fuel cells. Their research demonstrates the potential application of this technique to analysing battery materials, catalysts, and even cancer drug molecules.

Dr Michael Cherney – Professor Daniel Fisher | Unlocking Woolly Mammoth Mysteries: Tusks as Hormone Time Capsules

Dr Michael Cherney – Professor Daniel Fisher | Unlocking Woolly Mammoth Mysteries: Tusks as Hormone Time Capsules

The impressive tusks found on proboscideans (the order of mammals that includes elephants, woolly mammoths, and mastodons) are like time capsules, preserving detailed records of their bearers’ lives in the form of growth layers and chemical traces. Frozen in time for thousands of years, these layers can unlock secrets about the lives of long-extinct relatives of modern elephants. Dr Michael Cherney and Professor Daniel Fisher from the University of Michigan used innovative techniques to extract and analyse steroid hormones preserved in woolly mammoth tusks. This ground-breaking work opens new avenues for exploring the biology and behaviour of extinct species.

Professor Ken M Levy | The Boundaries of Free Will and Responsibility: From Academic Debate to the Real World

Professor Ken M Levy | The Boundaries of Free Will and Responsibility: From Academic Debate to the Real World

For almost thirty years, Professor Ken M Levy of Louisiana State University Law School has been thinking and writing about free will and responsibility. In several articles and his recent book, Free Will, Responsibility, and Crime: An Introduction (Routledge 2020), Professor Levy discusses a wide range of subjects, including the myth of the ‘self-made man’, whether psychopaths are culpable for their crimes, and the increasingly popular but highly controversial theory of responsibility scepticism. Professor Levy’s research has profound implications for law, ethics, and society.

Abordando el Aislamiento Social y la Depresión entre Mujeres Inmigrantes Mexicanas

Abordando el Aislamiento Social y la Depresión entre Mujeres Inmigrantes Mexicanas

Una gran cantidad de mujeres mexicanas sufren aislamiento y depresión después de llegar como inmigrantes a los Estados Unidos. Son particularmente vulnerables en el caso de carecer de conexiones sociales o una red de apoyo en su nuevo entorno. Un grupo inovador de investigación de la Universidad de Nuevo Mexico ha desarrollado una prometedora iniciativa llamada “Tertulias”,que ayuda a mejorar la salud mental y el bienestar de las mujeres inmigrantes.