Dynamic Hierarchical Reactive Controller Synthesis
Anne-Kathrin Schmuck, Rupak Majumdar

TL;DR
This paper introduces a hierarchical formalism and a dynamic synthesis algorithm for reactive controllers, enabling scalable and layered control strategies in complex hybrid systems by exploiting hierarchical game structures.
Contribution
It proposes a novel hierarchical modeling formalism and a dynamic synthesis procedure that efficiently constructs controllers for large-scale reactive systems with layered specifications.
Findings
Hierarchical game graphs reduce state space complexity.
The dynamic controller ensures local specifications are satisfied.
The approach is demonstrated on autonomous robot control in a building.
Abstract
In the formal approach to reactive controller synthesis, a symbolic controller for a possibly hybrid system is obtained by algorithmically computing a winning strategy in a two-player game. Such game-solving algorithms scale poorly as the size of the game graph increases. However, in many applications, the game graph has a natural hierarchical structure. In this paper, we propose a modeling formalism and a synthesis algorithm that exploits this hierarchical structure for more scalable synthesis. We define local games on hierarchical graphs as a modeling formalism which decomposes a large-scale reactive synthesis problem in two dimensions. First, the construction of a hierarchical game graph introduces abstraction layers, where each layer is again a two-player game graph. Second, every such layer is decomposed into multiple local game graphs, each corresponding to a node in the higher…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Logic, programming, and type systems
