Document Open Access Logo

On the Coalgebra of Partial Differential Equations

Author Michele Boreale

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2019.24.pdf
  • Filesize: 491 kB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Invariants
  • Theory of computation → Operational semantics
Keywords
  • coalgebra
  • partial differential equations
  • polynomials

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We note that the coalgebra of formal power series in commutative variables is final in a certain subclass of coalgebras. Moreover, a system Sigma of polynomial PDEs, under a coherence condition, naturally induces such a coalgebra over differential polynomial expressions. As a result, we obtain a clean coinductive proof of existence and uniqueness of solutions of initial value problems for PDEs. Based on this characterization, we give complete algorithms for checking equivalence of differential polynomial expressions, given Sigma.

Cite As Get BibTex

Michele Boreale. On the Coalgebra of Partial Differential Equations. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 24:1-24:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.MFCS.2019.24

Author Details

Michele Boreale
  • Università di Firenze, Dipartimento di Statistica, Informatica, Applicazioni (DiSIA) "G. Parenti", Viale Morgagni 65, I-50134 Firenze, Italy

Acknowledgements

Three anonymous reviewers have provided valuable comments.

References

  1. H. Bateman. Some recent researches on the motion of fluids. Monthly Weather Review, 43(4):163-170, 1915. Google Scholar
  2. S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, and P. Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325-352, 2014. Google Scholar
  3. F. Bonchi, M. M. Bonsangue, M. Boreale, J. J. M. M. Rutten, and A. Silva. A coalgebraic perspective on linear weighted automata. Inf. Comput., 211:77-105, 2012. Google Scholar
  4. M. Boreale. Weighted Bisimulation in Linear Algebraic Form. In CONCUR 2009, volume 5710 of LNCS, pages 163-177. Springer, 2009. Google Scholar
  5. M. Boreale. Algebra, coalgebra, and minimization in polynomial differential equations. In FoSSACS 2017, volume 10203 of LNCS, pages 71-87. Springer, 2017. Full version in Logical Methods in Computer Science 15(1) arXiv.org:1710.08350, 2019. Google Scholar
  6. M. Boreale. Algorithms for exact and approximate linear abstractions of polynomial continuous systems. In HSCC 2018, pages 207-216. ACM, 2018. Google Scholar
  7. M. Boreale. Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODE’s. In SOFSEM 2018: Theory and Practice of Computer Science - 44th International Conference on Current Trends in Theory and Practice of Computer Science, volume 10706 of LNCS, pages 442-455. Springer, 2018. Google Scholar
  8. F. Boulier, D. Lazard, F. Ollivier, and M. Petitot. Computing representations for radicals of finitely generated differential ideals. Appl. Algebra Engrg. Comm. Comput., 20(1):73-121, 2009. Google Scholar
  9. J. M. Burgers. A mathematical model illustrating the theory of turbulence. In Advances in applied mechanics, volume 1, pages 171-199. Elsevier, 1948. Google Scholar
  10. 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. Google Scholar
  11. K. Ghorbal and A. Platzer. Characterizing Algebraic Invariants by Differential Radical Invariants. In TACAS 2014, volume 8413 of LNCS, pages 279-294. Springer, 2014. URL: http://reports-archive.adm.cs.cmu.edu/anon/2013/CMU-CS-13-129.pdf.
  12. M. Janet. Sur les systèmes d'équations aux dérivées partielles. Thèses françaises de l'entre-deux-guerres. Gauthiers-Villars, Paris, 1920. URL: http://www.numdam.org/item?id=THESE_1920__19__1_0.
  13. D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. W. Leech, editor, Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967), pages 263-297. Pergamon, Oxford, 1970. Google Scholar
  14. E. R. Kolchin. Differential algebra and algebraic groups, volume 54 of Pure and Applied Mathematics. Academic Press, New York-London, 1973. Google Scholar
  15. H. Kong, S. Bogomolov, Ch. Schilling, Yu Jiang, and Th.A. Henzinger. Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters. In HSCC 2017, pages 163-172. ACM, 2017. Google Scholar
  16. F. Lemaire. Contribution à l'algorithmique en algèbre différentielle. Génie logiciel [cs.SE]. Université des Sciences et Technologie de Lille - Lille, 2002. URL: https://tel.archives-ouvertes.fr/tel-00001363/document.
  17. F. Lemaire. An Orderly Linear PDE System with Analytic Initial Conditions with a Non-analytic Solution. J. Symb. Comput., 35(5):487-498, May 2003. URL: https://doi.org/10.1016/S0747-7171(03)00017-8.
  18. M. Marvan. Sufficient Set of Integrability Conditions of an Orthonomic System. Foundations of Computational Mathematics, 9(6):651-674, 2009. Google Scholar
  19. D. Novikov and S. Yakovenko. Trajectories of polynomial vector fields and ascending chains of polynomial ideals. Annales de l'Institut Fourier, 49(2):563-609, 1999. URL: https://doi.org/10.5802/aif.1683.
  20. D. Pavlovic and M.H. Escardó. Calculus in Coinductive Form. In LICS 1998, pages 408-417. IEEE, 1998. Google Scholar
  21. A. Platzer. Logics of dynamical systems. In LICS 2012, pages 13-24. IEEE, 2012. Google Scholar
  22. A. Platzer. Differential hybrid games. ACM Trans. Comput. Log., 18(3):19-44, 2017. Google Scholar
  23. G. Reid, A. Wittkopf, and A. Boulton. Reduction of systems of nonlinear partial differential equations to simplified involutive forms. European Journal of Applied Mathematics, 7(6):635-666, 1996. Google Scholar
  24. C. Riquier. Les systèmes d'équations aux dérivèes partielles. Gauthiers-Villars, Paris, 1910. Google Scholar
  25. J. F. Ritt. Differential Algebra, volume XXXIII. American Mathematical Society Colloquium Publications, American Mathematical Society, New York, N. Y, 1950. Google Scholar
  26. C. J. Rust, G. J. Reid, and A. D. Wittkopf. Existence and Uniqueness Theorems for Formal Power Series Solutions of Analytic Differential Systems. In ISSAC 1999, pages 105-112, 1999. Google Scholar
  27. J. J. M. M. Rutten. Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science, 308(1-3):1-53, 2003. Google Scholar
  28. S. Sankaranarayanan. Automatic invariant generation for hybrid systems using ideal fixed points. In HSCC 2010, pages 221-230. ACM, 2010. Google Scholar
  29. S. Sankaranarayanan, H. Sipma, and Z. Manna. Non-linear loop invariant generation using Gröbner bases. In POPL 2004. ACM, 2004. Google Scholar
  30. J. M. Thomas. Differential Systems, volume XXI. American Mathematical Society Colloquium Publications, American Mathematical Society, New York, N. Y, 1937. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact