research-article

Algorithms for exact and approximate linear abstractions of polynomial continuous systems

Author:

Michele BorealeAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 207 - 216

https://doi.org/10.1145/3178126.3178137

Published: 11 April 2018 Publication History

Abstract

A polynomial continuous system S = (F,X0) is specified by a polynomial vector field F and a set of initial conditions X0. We study polynomial changes of bases that transform S into a linear system, called linear abstractions. We first give a complete algorithm to find all such abstractions that fit a user-specified template. This requires taking into account the algebraic structure of the set X0, which we do by working modulo an appropriate invariant ideal. Next, we give necessary and sufficient syntactic conditions under which a full linear abstraction exists, that is one capable of representing the behaviour of the individual variables in the original system. We then propose an approximate linearization and dimension-reduction technique, that is amenable to be implemented "on the fly". We finally illustrate the encouraging results of a preliminary experimentation with the linear abstraction algorithm, conducted on challenging systems drawn from the literature.

References

[1]

V.I. Arnold. Ordinary Differential Equations. The MIT Press, ISBN 0-262-51018-9, 1978.

[2]

Z. Bai, and D. Skoogh. A projection method for model reduction of bilinear dynamical systems. Linear Algebra Appl. 415(2- 3):406--425, 2006.

[3]

U. Baur, P. Benner, and L. Feng. Model Order Reduction for Linear and Nonlinear Systems: A System-Theoretic Perspective. Arch. Computat. Methods Eng. 21:331--358, 2014.

[4]

R. Bellman, J.M. Richardson. On some questions arising in the approximate solution of nonlinear differential equations. Quarterly of Applied Mathematics 20(4):333--339, Juanary, 1963.

[5]

M. L. Blinov, J. R. Faeder, B. Goldstein, and W. S. Hlavacek. BioNet-Gen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinformatics, 20(17): 3289--3291, 2004.

Digital Library

[6]

M. Boreale. Algebra, coalgebra, and minimization in polynomial differential equations. In Proc. of FoSSACS 2017, LNCS 10203:71--87, Springer, 2017.

Digital Library

[7]

M. Boreale. Complete algorithms for algebraic strongest post-conditions and weakest preconditions in polynomial ODE's. SOF-SEM'18, LNCS 10706:442--455, 2018. Full version available as CoRR, abs/1708.05377.

[8]

C. Chicone. Ordinary Differential Equations with Applications, 2/e. Texts in Applied Mathematics, Springer-Verlag, 2006.

[9]

D. Cox, J. Little, and D. O'Shea. Ideals, Varieties, and Algorithms An Introduction to Computational Algebraic Geometry and Commutative Algebra. Undergraduate Texts in Mathematics, Springer, 2007.

Digital Library

[10]

K. Ghorbal, A. Platzer. Characterizing Algebraic Invariants by Differential Radical Invariants. TACAS 2014, LNCS 8413:279--294, 2014.

[11]

A. Gil, J. Segura, and N.M. Temme. Numerical Methods for Special Functions. SIAM, 2007.

Digital Library

[12]

E. Goubault, J.-H. Jourdan, S. Putot, S. Sankaranarayanan. Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through Darboux polynomials. ACC 2014: 3571--3578, 2014.

[13]

H. Kong, S. Bogomolov, Ch. Schilling, Yu Jiang, Th.A. Henzinger. Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters. In HSCC 2017: 163--172, ACM, 2017.

Digital Library

[14]

K. Kowalski, W.-H. Steeb. Nonlinear Dynamical Systems and Carleman Linearization. World Scientific, 1991.

[15]

J.R. Phillips. Projection-based approaches for model reduction of weakly nonlinear time-varying systems. IEEE Trans. Comput.-Aided Des., vol. 22, no. 2, pp. 171--187, 2003.

Digital Library

[16]

A. Platzer. Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143--189, 2008.

Digital Library

[17]

R. Rebiha, A. V. Moura, and N. Matringe. Generating invariants for non-linear hybrid systems. Theoretical Computer Science, 594:180--200, 2015.

Digital Library

[18]

M. Rewienski and J. White. Atrajectory piecewise-linear approach to model order reduction and fast simulation of nonlinear circuits and micromachined devices. IEEE Trans. Comput.-Aided Des., vol. 22, no. 2, pp. 155--170, 2003.

Digital Library

[19]

Y. Saad. Iterative methods for sparse linear systems. SIAM, 2003.

Digital Library

[20]

S. Sankaranarayanan, H.B. Sipma, and Z. Manna. Non-linear loop invariant generation using Gröbner bases. POPL 2004: 318--329, ACM, 2004.

Digital Library

[21]

S. Sankaranarayanan, H.B. Sipma, and Z. Manna. Constructing invariants for hybrid systems. Formal Methods in System Design 32(1): 25--55, 2008.

Digital Library

[22]

S. Sankaranarayanan. Automatic invariant generation for hybrid systems using ideal fixed points. HSCC 2010: 221--230, 2010.

Digital Library

[23]

S. Sankaranarayanan. Automatic abstraction of non-linear systems using change of bases transformations. HSCC 2011: 143--152.

Digital Library

[24]

S. Sankaranarayanan. Change-Of-Bases Abstractions for Non-Linear Systems. CoRR abs/1204.4347, 2012.

[25]

A. Sogokon, K. Ghorbal, P.B. Jackson and A. Platzer. A method for invariant generation for polynomial continuous systems. VMCAI 2016, LNCS 9583:268--288. Springer, 2016.

Digital Library

[26]

R.F. Stengel. Flight Dynamics. Princeton University Press, 2004.

[27]

A. Tiwari, G. Khanna. Nonlinear systems: Approximating reach sets. In HSCC 2004:600--614, ACM, 2004.

Cited By

Fatnassi WShoukry Y(2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632970
Bacci GBacci GLarsen KSquillace GTribastone MTschaikowski MVandin A(2024)Dissimilarity for Linear Dynamical SystemsQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_8(125-142)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_8
Boreale M(2022)Automatic pre- and postconditions for partial differential equationsInformation and Computation10.1016/j.ic.2021.104860285(104860)Online publication date: May-2022
https://doi.org/10.1016/j.ic.2021.104860
Show More Cited By

Index Terms

Algorithms for exact and approximate linear abstractions of polynomial continuous systems
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Exact polynomial factorization by approximate high degree algebraic numbers
SNC '09: Proceedings of the 2009 conference on Symbolic numeric computation

For factoring polynomials in two variables with rational coefficients, an algorithm using transcendental evaluation was presented by Hulst and Lenstra. In their algorithm, transcendence measure was computed. However, a constant c is necessary to compute ...
Algorithms for exact polynomial root calculation

This thesis discusses two sets of fully specified algorithms which, given a univariate polynomial with integer coefficients (with possible multiple roots) and a positive rational error bound, uses infinite-precision arithmetic and Sturm's Theorem to ...
Automatic abstraction of non-linear systems using change of bases transformations
HSCC '11: Proceedings of the 14th international conference on Hybrid systems: computation and control

We present abstraction techniques that transform a given non-linear dynamical system into a linear system, such that, invariant properties of the resulting linear abstraction can be used to infer invariants for the original system. The abstraction ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
118
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Fatnassi WShoukry Y(2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632970
Bacci GBacci GLarsen KSquillace GTribastone MTschaikowski MVandin A(2024)Dissimilarity for Linear Dynamical SystemsQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_8(125-142)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_8
Boreale M(2022)Automatic pre- and postconditions for partial differential equationsInformation and Computation10.1016/j.ic.2021.104860285(104860)Online publication date: May-2022
https://doi.org/10.1016/j.ic.2021.104860
Boreale MCollodi L(2022)Linearization, Model Reduction and Reachability in Nonlinear odesReachability Problems10.1007/978-3-031-19135-0_4(49-66)Online publication date: 12-Oct-2022
https://doi.org/10.1007/978-3-031-19135-0_4
Bacci GBacci GLarsen KTribastone MTschaikowski MVandin AGorla D(2021)Efficient local computation of differential bisimulations via coupling and up-to methodsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470555(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470555
He HWu J(2020)A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances MethodInformation10.3390/info1105024611:5(246)Online publication date: 2-May-2020
https://doi.org/10.3390/info11050246
Boreale M(2020)Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial odesScience of Computer Programming10.1016/j.scico.2020.102441(102441)Online publication date: Mar-2020
https://doi.org/10.1016/j.scico.2020.102441
Boreale M(2020)Automatic Pre- and Postconditions for Partial Differential EquationsQuantitative Evaluation of Systems10.1007/978-3-030-59854-9_15(193-210)Online publication date: 3-Nov-2020
https://doi.org/10.1007/978-3-030-59854-9_15

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten