This program is tentative and subject to change.
Control problems for embedded systems like cars and trains can be modeled by two-player hybrid games. Control envelopes, which are families of safe control solutions, correspond to nondeterministic policies that ensure a player following them will not lose. Each deterministic, finite specialization of the nondeterministic policy is a control solution. This paper synthesizes control envelopes for hybrid games that are as permissive as possible. It introduces subvalue maps, a compositional representation of such policies that enables verification and synthesis along the structure of the game. An inductive logical characterization in differential game logic (dGL) checks whether a subvalue map induces a sound control envelope which ensures that the player never loses, no matter what actions the opponent plays. The maximal subvalue map, which allows the most action options while still winning, is shown to exist and satisfy a logical characterization. An inductive subvalue map synthesis framework is obtained from the soundness characterization. An evaluation of the framework uses the significant expressivity of dGL to model and solve a broad range of control challenges.
This program is tentative and subject to change.
Mon 5 OctDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | Synthesis and SpecificationOOPSLA at Junior Ballroom 1&2 Chair(s): Jocelyn Qiaochu Chen University of Alberta | ||
10:30 18mTalk | Grammar Repair with Examples and Tree Automata OOPSLA Yunjeong Lee National University of Singapore, Gokul Rajiv National University of Singapore, Ilya Sergey National University of Singapore DOI | ||
10:48 18mTalk | Hybrid Game Control Envelope Synthesis OOPSLA Aditi Kabra Carnegie Mellon University, Jonathan Laurent KIT, Stefan Mitsch DePaul University, André Platzer KIT DOI | ||
11:06 18mTalk | P4-SpecTec: Integrating a Language Mechanization Framework into the Real-World P4 Specification OOPSLA DOI | ||
11:24 18mTalk | Commit-Window Observation Contracts for Reactive Entity-Component Systems OOPSLA DOI | ||
11:42 18mTalk | Incremental Program Synthesis from Event Logs OOPSLA Jinwoo Kim University of California at San Diego, Victor Nicolet Amazon, Joey Dodds Amazon, Loris D'Antoni University of California at San Diego DOI | ||