Document Open Access Logo

Algebraic Invariants for Linear Hybrid Automata

Authors Rupak Majumdar, Joël Ouaknine, Amaury Pouly , James Worrell

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.32.pdf
  • Filesize: 0.55 MB
  • 17 pages

Document Identifiers

Author Details

Rupak Majumdar
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Joël Ouaknine
  • Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany
  • Department of Computer Science, Oxford University, UK
Amaury Pouly
  • Université de Paris, IRIF, CNRS, F-75013 Paris, France
James Worrell
  • Department of Computer Science, Oxford University, UK

Funding

  • Majumdar, Rupak: Supported by the European Research Council under Grant Agreement 610150 (ERC Synergy Grant ImPACT) and DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
  • Ouaknine, Joël: Supported by ERC grant AVS-ISS (648701) and DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
  • Pouly, Amaury: Part of this work was done at MPI-SWS.
  • Worrell, James: Supported by EPSRC Fellowship EP/N008197/1.

Acknowledgements

We thank Khalil Ghorbal for helpful discussions on the subject of this paper.

Cite As Get BibTex

Rupak Majumdar, Joël Ouaknine, Amaury Pouly, and James Worrell. Algebraic Invariants for Linear Hybrid Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.32

Abstract

We exhibit an algorithm to compute the strongest algebraic (or polynomial) invariants that hold at each location of a given guard-free linear hybrid automaton (i.e., a hybrid automaton having only unguarded transitions, all of whose assignments are given by affine expressions, and all of whose continuous dynamics are given by linear differential equations). Our main tool is a control-theoretic result of independent interest: given such a linear hybrid automaton, we show how to discretise the continuous dynamics in such a way that the resulting automaton has precisely the same algebraic invariants.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Models of computation
Keywords
  • Hybrid automata
  • algebraic invariants

Metrics

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

References

  1. Hirokazu Anai and Volker Weispfenning. Reach set computations using real quantifier elimination. In Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings, volume 2034 of Lecture Notes in Computer Science, pages 63-76. Springer, 2001. Google Scholar
  2. Michele Boreale. Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial odes. Sci. Comput. Program., 193:102441, 2020. Google Scholar
  3. H. Derksen, E. Jeandel, and P. Koiran. Quantum automata and algebraic groups. J. Symb. Comput., 39(3-4):357-371, 2005. Google Scholar
  4. Stephan Falke and Deepak Kapur. When is a formula a loop invariant? In Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, volume 9200 of Lecture Notes in Computer Science, pages 264-286. Springer, 2015. Google Scholar
  5. Khalil Ghorbal and André Platzer. Characterizing algebraic invariants by differential radical invariants. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pages 279-294. Springer, 2014. Google Scholar
  6. Thomas A. Henzinger. The theory of hybrid automata. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 278-292. IEEE Computer Society, 1996. Google Scholar
  7. Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell. Polynomial invariants for affine programs. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 530-539, 2018. Google Scholar
  8. Z. Kincaid, J. Cyphert, J. Breck, and T. W. Reps. Non-linear reasoning for invariant synthesis. PACMPL, 2(POPL):54:1-54:33, 2018. Google Scholar
  9. Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. Symbolic reachability computation for families of linear vector fields. J. Symb. Comput., 32(3):231-253, 2001. URL: https://doi.org/10.1006/jsco.2001.0472.
  10. Daniel Liberzon. Switching in Systems and Control. Birkhauser/Springer, 2003. Google Scholar
  11. D. W. Masser. Linear relations on algebraic groups. In New Advances in Transcendence Theory. Cambridge University Press, 1988. Google Scholar
  12. Joël Ouaknine, Amaury Pouly, João Sousa Pinto, and James Worrell. Solvability of matrix-exponential equations. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 798-806, 2016. Google Scholar
  13. Enric Rodríguez-Carbonell and Deepak Kapur. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program., 64(1):54-75, 2007. URL: https://doi.org/10.1016/j.scico.2006.03.003.
  14. Enric Rodríguez-Carbonell and Deepak Kapur. Generating all polynomial invariants in simple loops. J. Symb. Comput., 42(4):443-476, 2007. URL: https://doi.org/10.1016/j.jsc.2007.01.002.
  15. Enric Rodríguez-Carbonell and Ashish Tiwari. Generating polynomial invariants for hybrid systems. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems: Computation and Control, pages 590-605, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  16. Sriram Sankaranarayanan. Automatic invariant generation for hybrid systems using ideal fixed points. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010, pages 221-230. ACM, 2010. Google Scholar
  17. Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Constructing invariants for hybrid systems. Formal Methods in System Design, 32(1):25-55, 2008. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact