Skip to content

Research at St Andrews

Model checking cancer automata

Research output: ResearchConference contribution


Open Access permissions



School/Research organisations


Cancer is a chronic disease where cells grow and multiply in an uncontrollable manner ultimately spreading and invading surrounding tissue, and metastasising in other parts or organs of the body. Automata can be used to capture cancer
evolving through a (discrete finite) sequence of progressive stages called phenotypes. Automata consist of states (known as hallmarks of cancer) and transitions between states, indicating a progression or regression of the cancer. We explore extensions and combinations of different variants of timed automata
and associated tools to model and analyse a model of the disease in different ways. We combine patient information and comorbidities with the cancer automaton through composition. The goal of this work is to use model checking as an analysis technique to provide further insights into the effectiveness of treatment plans for a given patient, and how these could potentially inhibit or slow down the progression of cancer.


Original languageEnglish
Title of host publicationIEEE EMBS International Conference on Biomedical and Health Informatics, BHI 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781509024551
StatePublished - 18 Apr 2016
Event3rd IEEE EMBS International Conference on Biomedical and Health Informatics, BHI 2016 - The Westin Las Vegas Hotel, Las Vegas, United States
Duration: 24 Feb 201627 Feb 2016


Conference3rd IEEE EMBS International Conference on Biomedical and Health Informatics, BHI 2016
CountryUnited States
CityLas Vegas
Internet address

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. An integrated framework for verifying multiple care pathways

    Bowles, J. K. F., Caminati, M. B. & Cha, S. 13 Sep 2017 Eleventh International Symposium on Theoretical Aspects of Software Engineering. IEEE Computer Society, 8 p.

    Research output: ResearchConference contribution

  2. Estimating capacity and resource allocation in healthcare settings using business process modelling and simulation

    Redeker, G., Webber, T., Czekster, R., Quickert, S. & Bowles, J. K. F. 2 Jul 2017 Anais XXXVII Congresso da Sociedade Brasileira de Computação. Sociedade Brasileira de Computação (SBC), p. 1979-1982

    Research output: ResearchConference contribution

  3. Weaving true-concurrent aspects using constraint solvers

    Bowles, J. K. F., Bordbar, B. & Alwanain, M. 3 Feb 2017 2016 16th International Conference on Application of Concurrency to System Design (ACSD). IEEE Computer Society, p. 35-44 10 p. 7842499

    Research output: ResearchConference contribution

  4. Formal verification of CNL health recommendations

    Rahman, F. & Bowles, J. K. F. 2017 Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. Polikarpova, N. & Schneider, S. (eds.). Cham: Springer, p. 357-371 15 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 10510)

    Research output: ResearchConference contribution

  5. A flexible approach for finding optimal paths with minimal conflicts

    Bowles, J. K. F. & Caminati, M. B. 2017 Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings. Duan, Z. & Ong, L. (eds.). Springer, p. 209-225 16 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 10610)

    Research output: ResearchConference contribution

ID: 240664699