Discretization of Continuous Dynamical Systems Using UPPAAL

Abstract

We want to enable the analysis of continuous dynamical systems (where the evolution of a vector of continuous state variables is described by differential equations) by model checking. We do this by showing how such a dynamical system can be translated into a discrete model of communicating timed automata that can be analyzed by the UPPAAL tool. The basis of the translation is the well-known Euler approach for solving differential equations where we use fixed discrete value steps instead of fixed time steps. Each state variable is represented by a timed automaton in which the delay for taking the next value is calculated on the fly using the differential equations. The state variable automata proceed independently but may notify each other when a value step has been completed; this leads to a recalculation of delays. The approach has been implemented in the tool ANIMO for analyzing biological kinase networks in cells. This tool has been used in actual biological research on osteoarthritis dealing with systems where the dimension of the state vector (the number of nodes in the network) is in the order of one hundred.
Original languageEnglish
Title of host publicationModelEd, TestEd, TrustEd
Subtitle of host publicationEssays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday
EditorsJoost-Pieter Katoen, Rom Langerak, Arend Rensink
PublisherSpringer
Pages297-315
Number of pages19
ISBN (Electronic)978-3-319-68270-9
ISBN (Print)978-3-319-68269-3
DOIs
StatePublished - 27 Sep 2017

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10500
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dynamical systems
Differential equations
Model checking

Keywords

  • Discretization
  • Euler method
  • Model Checking
  • Timed Automata
  • Systems Biology

Cite this

Schivo, S., & Langerak, R. (2017). Discretization of Continuous Dynamical Systems Using UPPAAL. In J-P. Katoen, R. Langerak, & A. Rensink (Eds.), ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday (pp. 297-315). (Lecture Notes in Computer Science; Vol. 10500). Springer. DOI: 10.1007/978-3-319-68270-9_15

Schivo, Stefano ; Langerak, Romanus / Discretization of Continuous Dynamical Systems Using UPPAAL.

ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday. ed. / Joost-Pieter Katoen; Rom Langerak; Arend Rensink. Springer, 2017. p. 297-315 (Lecture Notes in Computer Science; Vol. 10500).

Research output: Scientific - peer-reviewChapter

@inbook{8e1537b83bff400cbf0a6cf88be700e4,
title = "Discretization of Continuous Dynamical Systems Using UPPAAL",
abstract = "We want to enable the analysis of continuous dynamical systems (where the evolution of a vector of continuous state variables is described by differential equations) by model checking. We do this by showing how such a dynamical system can be translated into a discrete model of communicating timed automata that can be analyzed by the UPPAAL tool. The basis of the translation is the well-known Euler approach for solving differential equations where we use fixed discrete value steps instead of fixed time steps. Each state variable is represented by a timed automaton in which the delay for taking the next value is calculated on the fly using the differential equations. The state variable automata proceed independently but may notify each other when a value step has been completed; this leads to a recalculation of delays. The approach has been implemented in the tool ANIMO for analyzing biological kinase networks in cells. This tool has been used in actual biological research on osteoarthritis dealing with systems where the dimension of the state vector (the number of nodes in the network) is in the order of one hundred.",
keywords = "Discretization, Euler method, Model Checking, Timed Automata, Systems Biology",
author = "Stefano Schivo and Romanus Langerak",
year = "2017",
month = "9",
doi = "10.1007/978-3-319-68270-9_15",
isbn = "978-3-319-68269-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "297--315",
editor = "Joost-Pieter Katoen and Rom Langerak and Arend Rensink",
booktitle = "ModelEd, TestEd, TrustEd",

}

Schivo, S & Langerak, R 2017, Discretization of Continuous Dynamical Systems Using UPPAAL. in J-P Katoen, R Langerak & A Rensink (eds), ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 10500, Springer, pp. 297-315. DOI: 10.1007/978-3-319-68270-9_15

Discretization of Continuous Dynamical Systems Using UPPAAL. / Schivo, Stefano ; Langerak, Romanus .

ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday. ed. / Joost-Pieter Katoen; Rom Langerak; Arend Rensink. Springer, 2017. p. 297-315 (Lecture Notes in Computer Science; Vol. 10500).

Research output: Scientific - peer-reviewChapter

TY - CHAP

T1 - Discretization of Continuous Dynamical Systems Using UPPAAL

AU - Schivo,Stefano

AU - Langerak,Romanus

PY - 2017/9/27

Y1 - 2017/9/27

N2 - We want to enable the analysis of continuous dynamical systems (where the evolution of a vector of continuous state variables is described by differential equations) by model checking. We do this by showing how such a dynamical system can be translated into a discrete model of communicating timed automata that can be analyzed by the UPPAAL tool. The basis of the translation is the well-known Euler approach for solving differential equations where we use fixed discrete value steps instead of fixed time steps. Each state variable is represented by a timed automaton in which the delay for taking the next value is calculated on the fly using the differential equations. The state variable automata proceed independently but may notify each other when a value step has been completed; this leads to a recalculation of delays. The approach has been implemented in the tool ANIMO for analyzing biological kinase networks in cells. This tool has been used in actual biological research on osteoarthritis dealing with systems where the dimension of the state vector (the number of nodes in the network) is in the order of one hundred.

AB - We want to enable the analysis of continuous dynamical systems (where the evolution of a vector of continuous state variables is described by differential equations) by model checking. We do this by showing how such a dynamical system can be translated into a discrete model of communicating timed automata that can be analyzed by the UPPAAL tool. The basis of the translation is the well-known Euler approach for solving differential equations where we use fixed discrete value steps instead of fixed time steps. Each state variable is represented by a timed automaton in which the delay for taking the next value is calculated on the fly using the differential equations. The state variable automata proceed independently but may notify each other when a value step has been completed; this leads to a recalculation of delays. The approach has been implemented in the tool ANIMO for analyzing biological kinase networks in cells. This tool has been used in actual biological research on osteoarthritis dealing with systems where the dimension of the state vector (the number of nodes in the network) is in the order of one hundred.

KW - Discretization

KW - Euler method

KW - Model Checking

KW - Timed Automata

KW - Systems Biology

U2 - 10.1007/978-3-319-68270-9_15

DO - 10.1007/978-3-319-68270-9_15

M3 - Chapter

SN - 978-3-319-68269-3

T3 - Lecture Notes in Computer Science

SP - 297

EP - 315

BT - ModelEd, TestEd, TrustEd

PB - Springer

ER -

Schivo S, Langerak R. Discretization of Continuous Dynamical Systems Using UPPAAL. In Katoen J-P, Langerak R, Rensink A, editors, ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday. Springer. 2017. p. 297-315. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-68270-9_15