TY - GEN
T1 - Inner and outer approximating flowpipes for delay differential equations
AU - Goubault, Eric
AU - Putot, Sylvie
AU - Sahlmann, Lorenz
N1 - Publisher Copyright:
© The Author(s) 2018.
PY - 2018/1/1
Y1 - 2018/1/1
N2 - Delay differential equations are fundamental for modeling networked control systems where the underlying network induces delay for retrieving values from sensors or delivering orders to actuators. They are notoriously difficult to integrate as these are actually functional equations, the initial state being a function. We propose a scheme to compute inner and outer-approximating flowpipes for such equations with uncertain initial states and parameters. Inner-approximating flowpipes are guaranteed to contain only reachable states, while outer-approximating flowpipes enclose all reachable states. We also introduce a notion of robust inner-approximation, which we believe opens promising perspectives for verification, beyond property falsification. The efficiency of our approach relies on the combination of Taylor models in time, with an abstraction or parameterization in space based on affine forms, or zonotopes. It also relies on an extension of the mean-value theorem, which allows us to deduce inner-approximating flowpipes, from flowpipes outer-approximating the solution of the DDE and its Jacobian with respect to constant but uncertain parameters and initial conditions. We present some experimental results obtained with our C++ implementation.
AB - Delay differential equations are fundamental for modeling networked control systems where the underlying network induces delay for retrieving values from sensors or delivering orders to actuators. They are notoriously difficult to integrate as these are actually functional equations, the initial state being a function. We propose a scheme to compute inner and outer-approximating flowpipes for such equations with uncertain initial states and parameters. Inner-approximating flowpipes are guaranteed to contain only reachable states, while outer-approximating flowpipes enclose all reachable states. We also introduce a notion of robust inner-approximation, which we believe opens promising perspectives for verification, beyond property falsification. The efficiency of our approach relies on the combination of Taylor models in time, with an abstraction or parameterization in space based on affine forms, or zonotopes. It also relies on an extension of the mean-value theorem, which allows us to deduce inner-approximating flowpipes, from flowpipes outer-approximating the solution of the DDE and its Jacobian with respect to constant but uncertain parameters and initial conditions. We present some experimental results obtained with our C++ implementation.
UR - https://www.scopus.com/pages/publications/85051124112
U2 - 10.1007/978-3-319-96142-2_31
DO - 10.1007/978-3-319-96142-2_31
M3 - Conference contribution
AN - SCOPUS:85051124112
SN - 9783319961415
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 523
EP - 541
BT - Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
A2 - Weissenbacher, Georg
A2 - Chockler, Hana
PB - Springer Verlag
T2 - 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
Y2 - 14 July 2018 through 17 July 2018
ER -