Document Open Access Logo

Refining Constructive Hybrid Games

Authors Rose Bohrer , André Platzer

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.14.pdf
  • Filesize: 0.63 MB
  • 19 pages

Document Identifiers

Author Details

Rose Bohrer
  • Carnegie Mellon University, Pittsburgh, PA, USA
André Platzer
  • Carnegie Mellon University, Pittsburgh, PA, USA
  • Technische Universität München, Germany

Funding

This research was sponsored by the AFOSR under grant number FA9550-16-1-0288.
  • Bohrer, Rose: The first author was also funded by the NDSEG Fellowship.

Acknowledgements

We thank Jon Sterling for suggestions regarding our choice of type theory and for references to the literature. We thank the anonymous reviewers for their helpful feedback.

Cite AsGet BibTex

Rose Bohrer and André Platzer. Refining Constructive Hybrid Games. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.14

Abstract

We extend the constructive differential game logic (CdGL) of hybrid games with a refinement connective that relates two hybrid games. In addition to CdGL’s ability to prove the existence of winning strategies for specific postconditions of hybrid games, game refinements relate two games to one another. That makes it possible to prove that any winning strategy for any postcondition of one game carries over to a winning strategy for the other. Since CdGL is constructive, a computable winning strategy can be extracted from a proof that a player wins a game. A folk theorem says that any such winning strategy for a hybrid game gives rise to a corresponding hybrid system satisfying the same property. We make this precise using CdGL’s game refinements and prove correct the construction of hybrid systems from winning strategies of hybrid games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • Hybrid Games
  • Constructive Logic
  • Refinement
  • Game Logic

Metrics

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

Related Versions

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. URL: https://doi.org/10.1006/inco.2000.2930.
  2. Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. URL: https://doi.org/10.1017/CBO9781139195881.
  3. Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In LICS, pages 303-310. IEEE, 2001. URL: https://doi.org/10.1109/LICS.2001.932506.
  4. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
  5. Ralph-Johan Back and Joakim von Wright. Refinement Calculus - A Systematic Introduction. Graduate Texts in Computer Science. Springer, 1998. URL: https://doi.org/10.1007/978-1-4612-1674-2.
  6. Richard Banach, Michael J. Butler, Shengchao Qin, Nitika Verma, and Huibiao Zhu. Core Hybrid Event-B I: Single Hybrid Event-B machines. Sci. Comput. Program., 105:92-123, 2015. URL: https://doi.org/10.1016/j.scico.2015.02.003.
  7. Amit Bhatia, Lydia E. Kavraki, and Moshe Y. Vardi. Motion planning with hybrid dynamics and temporal goals. In Conference on Decision and Control, pages 1108-1115. IEEE, 2010. URL: https://doi.org/10.1109/CDC.2010.5717440.
  8. Errett Bishop. Foundations of constructive analysis. McGraw-Hill, 1967. Google Scholar
  9. Rose Bohrer and André Platzer. Toward structured proofs for dynamic logics. CoRR, abs/1908.05535, 2019. URL: http://arxiv.org/abs/1908.05535.
  10. Rose Bohrer and André Platzer. Constructive game logic. In Peter Müller, editor, ESOP, volume 12075 of LNCS. Springer, 2020. URL: http://arxiv.org/abs/2002.08523.
  11. Rose Bohrer and André Platzer. Constructive hybrid games. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR, LNCS. Springer, 2020. Google Scholar
  12. Rose Bohrer and André Platzer. Refining constructive hybrid games. CoRR, abs/2002.02576, 2020. URL: http://arxiv.org/abs/2002.02576.
  13. Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer. VeriPhy: Verified controller executables from verified cyber-physical system models. In Dan Grossman, editor, PLDI, pages 617-630. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192406.
  14. Douglas S Bridges and Luminita Simona Vita. Techniques of constructive analysis. Springer, 2007. Google Scholar
  15. Sergio A. Celani. A fragment of intuitionistic dynamic logic. Fundam. Inform., 46(3):187-197, 2001. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi46-3-01.
  16. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR, volume 4703 of LNCS, pages 59-73. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74407-8_5.
  17. Thierry Coquand and Gérard P. Huet. The calculus of constructions. Inf. Comput., 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  18. Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, COLOG, volume 417 of LNCS, pages 50-66. Springer, 1988. URL: https://doi.org/10.1007/3-540-52335-9_47.
  19. Luís Cruz-Filipe, Herman Geuvers, and Freek Wiedijk. C-CoRN, the constructive Coq repository at Nijmegen. In Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec, editors, MKM, volume 3119 of LNCS. Springer, 2004. Accessed: commits 9c44dae and 6411967. URL: https://doi.org/10.1007/978-3-540-27818-4_7.
  20. JW Degen and JM Werner. Towards intuitionistic dynamic logic. Log. and Log. Philosophy, 15(4):305-324, 2006. URL: https://doi.org/10.12775/LLP.2006.018.
  21. Peter Dybjer. Inductive families. Formal Asp. Comput., 6(4):440-465, 1994. URL: https://doi.org/10.1007/BF01211308.
  22. Sebastian Enqvist, Helle Hvid Hansen, Clemens Kupke, Johannes Marti, and Yde Venema. Completeness for game logic. In LICS, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785676.
  23. Georgios E. Fainekos, Antoine Girard, Hadas Kress-Gazit, and George J. Pappas. Temporal logic motion planning for dynamic robots. Automatica, 45(2):343-352, 2009. URL: https://doi.org/10.1016/j.automatica.2008.08.008.
  24. Ioannis Filippidis, Sumanth Dathathri, Scott C. Livingston, Necmiye Ozay, and Richard M. Murray. Control design for hybrid systems with TuLiP: The temporal logic planning toolbox. In Conference on Control Applications, pages 1030-1041. IEEE, 2016. URL: https://doi.org/10.1109/CCA.2016.7587949.
  25. Cameron Finucane, Gangyuan Jing, and Hadas Kress-Gazit. LTLMoP: Experimenting with language, temporal logic and robot control. In IROS, pages 1988-1993. IEEE, 2010. URL: https://doi.org/10.1109/IROS.2010.5650371.
  26. John Nathan Foster. Bidirectional programming languages. Technical Report MS-CIS-10-08, Department of Computer & Information Science, University of Pennsylvania, Philadelphia, PA, March 2010. Google Scholar
  27. Sujata Ghosh. Strategies made explicit in dynamic game logic. Workshop on Logic and Intelligent Interaction at ESSLLI, Hamburg, pages 74-81, 2008. Google Scholar
  28. Valentin Goranko. The basic algebra of game equivalences. Studia Logica, 75(2):221-238, 2003. URL: https://doi.org/10.1023/A:1027311011342.
  29. David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic logic. MIT Press, 2000. URL: https://doi.org/10.1145/568438.568456.
  30. George Edward Hughes and Max Cresswell. A new introduction to modal logic. Routledge, 1996. Google Scholar
  31. Norihiro Kamide. Strong normalization of program-indexed lambda calculus. Bull. Sect. Log. Univ. Łódź, 39(1-2):65-78, 2010. Google Scholar
  32. Marius Kloetzer and Calin Belta. A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans. Automat. Contr., 53(1):287-297, 2008. URL: https://doi.org/10.1109/TAC.2007.914952.
  33. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  34. Dexter Kozen. Kleene algebra with tests. ACM Trans. Program. Lang. Syst., 19(3):427-443, 1997. Google Scholar
  35. James Lipton. Constructive Kripke semantics and realizability. In Y. N. Moschovakis, editor, Logic from Computer Science, pages 319-357. Springer, 1992. URL: https://doi.org/10.1017/978-1-4612-2822-6_13.
  36. Sarah M. Loos and André Platzer. Differential refinement logic. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, LICS, pages 505-514. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934555.
  37. Evgeny Makarov and Bas Spitters. The Picard algorithm for ordinary differential equations in Coq. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP, volume 7998 of LNCS. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_34.
  38. Konstantinos Mamouras. Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism. Log. Methods Comput. Sci., 12(3):1-41, 2016. URL: https://doi.org/10.2168/LMCS-12(3:6)2016.
  39. Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyber-physical system models. Form. Methods Syst. Des., 49(1):33-74, 2016. URL: https://doi.org/10.1007/s10703-016-0241-z.
  40. Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. J. Funct. Program., 18(5-6):865-911, 2008. URL: https://doi.org/10.1017/S0956796808006953.
  41. Rohit Parikh. Propositional game logic. In FOCS, pages 195-200. IEEE, 1983. URL: https://doi.org/10.1109/SFCS.1983.47.
  42. André Platzer. Differential dynamic logic for hybrid systems. J. Autom. Reas., 41(2):143-189, 2008. URL: https://doi.org/10.1007/s10817-008-9103-8.
  43. André Platzer. The structure of differential invariants and differential cut elimination. Log. Methods Comput. Sci., 8(4):1-38, 2012. URL: https://doi.org/10.2168/LMCS-8(4:16)2012.
  44. André Platzer. Differential game logic. ACM Trans. Comput. Log., 17(1):1:1-1:51, 2015. URL: https://doi.org/10.1145/2817824.
  45. André Platzer. Differential hybrid games. ACM Trans. Comput. Log., 18(3):19:1-19:44, 2017. URL: https://doi.org/10.1145/3091123.
  46. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, Switzerland, 2018. URL: https://doi.org/10.1007/978-3-319-63588-0.
  47. André Platzer and Yong Kiam Tan. Differential equation invariance axiomatization. J. ACM, 67(1), 2020. URL: https://doi.org/10.1145/3380825.
  48. Ramaswamy Ramanujam and Sunil Easaw Simon. Dynamic logic on games with structured strategies. In Gerhard Brewka and Jérôme Lang, editors, Knowledge Representation, pages 49-58. AAAI Press, 2008. URL: http://www.aaai.org/Library/KR/2008/kr08-006.php.
  49. Ankur Taly and Ashish Tiwari. Switching logic synthesis for reachability. In Luca P. Carloni and Stavros Tripakis, editors, EMSOFT, pages 19-28. ACM, 2010. URL: https://doi.org/10.1145/1879021.1879025.
  50. The Coq development team. The Coq proof assistant reference manual, 2019. URL: https://coq.inria.fr/.
  51. Johan Van Benthem. Games in dynamic-epistemic logic. Bull. Econ. Research, 53(4):219-248, 2001. Google Scholar
  52. Johan van Benthem. Logic of strategies: What and how? In Johan van Benthem, Sujata Ghosh, and Rineke Verbrugge, editors, Models of Strategic Reasoning - Logics, Games, and Communities, volume 8972 of LNCS, pages 321-332. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48540-8_10.
  53. Johan van Benthem and Eric Pacuit. Dynamic logics of evidence-based beliefs. Studia Logica, 99(1-3):61-92, 2011. URL: https://doi.org/10.1007/s11225-011-9347-x.
  54. Johan van Benthem, Eric Pacuit, and Olivier Roy. Toward a theory of play: A logical perspective on games and interaction. Games, 2011. URL: https://doi.org/10.3390/g2010052.
  55. Wiebe van der Hoek, Wojciech Jamroga, and Michael J. Wooldridge. A logic for strategic reasoning. In Frank Dignum, Virginia Dignum, Sven Koenig, Sarit Kraus, Munindar P. Singh, and Michael J. Wooldridge, editors, AAMAS. ACM, 2005. URL: https://doi.org/10.1145/1082473.1082497.
  56. Jaap van Oosten. Realizability: A historical essay. Math. Structures Comput. Sci., 12(3):239-263, 2002. URL: https://doi.org/10.1017/S0960129502003626.
  57. Klaus Weihrauch. Computable Analysis - An Introduction. Texts in Theoretical Computer Science. Springer, 2000. URL: https://doi.org/10.1007/978-3-642-56999-9.
  58. Duminda Wijesekera. Constructive modal logics I. Ann. Pure Appl. Log., 50(3):271-301, 1990. URL: https://doi.org/10.1016/0168-0072(90)90059-B.
  59. Duminda Wijesekera and Anil Nerode. Tableaux for constructive concurrent dynamic logic. Ann. Pure Appl. Log., 135(1-3):1-72, 2005. URL: https://doi.org/10.1016/j.apal.2004.12.001.
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 Imprint Privacy Contact