Dynamic hierarchical reactive controller synthesis. (English) Zbl 1379.93048

Summary: 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 that 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 level game graph. While local games have the potential to reduce the state space for controller synthesis, they lead to more complex synthesis problems where strategies computed for one local game can impose additional requirements on lower-level local games. Our second contribution is a procedure to construct a dynamic controller for local game graphs over hierarchies. The controller computes assume-admissible winning strategies that satisfy local specifications in the presence of environment assumptions, and dynamically updates specifications and strategies due to interactions between games at different abstraction layers at each step of the play. We show that our synthesis procedure is sound: the controller constructs a play that satisfies all local specifications. We illustrate our results through an example controlling an autonomous robot in a building with known floor plan and provide simulation results using an implementation of our algorithm on top of LTLMoP.


93B40 Computational methods in systems theory (MSC2010)
93A15 Large-scale systems
93A13 Hierarchical systems
93B50 Synthesis problems
91A65 Hierarchical games (including Stackelberg games)
93C85 Automated systems (robots, etc.) in control theory
94C15 Applications of graph theory to circuits and networks
03B44 Temporal logic


Full Text: DOI arXiv


[1] Abadi, M; Lamport, L, The existence of refinement mappings, Theor Comput Sci, 82, 253-284, (1991) · Zbl 0728.68083
[2] Alur, R; La Torre, S; Madhusudan, P, Modular strategies for recursive game graphs, 363-378, (2003) · Zbl 1031.68048
[3] Bloem, R; Jobstmann, B; Piterman, N; Pnueli, A; Saar, Y, Synthesis of reactive(1) designs, J Comput Syst Sci, 78, 911-938, (2012) · Zbl 1247.68050
[4] Bloem, R; Ehlers, R; Jacobs, S; Könighofer, R, How to handle assumptions in synthesis, 34-50, (2014)
[5] Bloem, R; Ehlers, R; Könighofer, R, Cooperative reactive synthesis, 394-410, (2015) · Zbl 1471.68131
[6] Brenguier R, Raskin J-F, Sassolas M (2014) The complexity of admissibility in omega-regular games CSL-LICS, vol 23, pp 1-10 · Zbl 1401.68110
[7] Brenguier, R; Raskin, J-F; Sankur, O, Assume-admissible synthesis, (2015) · Zbl 1374.68322
[8] Cousot P, Cousot R (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints POPL 77. ACM, pp 238-252
[9] De Crescenzo, I; La Torre, S, Modular synthesis with open components, 96-108, (2013) · Zbl 1407.68286
[10] Emerson, E; Jutla, C, Tree automata, mu-calculus and determinacy, 368-377, (1991)
[11] Erol K, Hendler JA, Nau DS (1995) Semantics for hierarchical task-network planning. Technical report, University of Maryland · Zbl 1044.93502
[12] Finucane, C; Jing, G; Kress-Gazit, H, Ltlmop experimenting with language, temporal logic and robot control, 1988-1993, (2010)
[13] Girard, A; Pappas, G, Hierarchical control system design using approximate simulation, Automatica, 45, 566-571, (2009) · Zbl 1158.93301
[14] Henzinger TA, Majumdar R, Mang F, Raskin J-f (2000) Abstract interpretation of game properties Static analysis, LNCS, vol 1824, pp 220-239 · Zbl 0966.68150
[15] Hess, D; Althoff, M; Sattel, T, Formal verification of maneuver automata for parameterized motion primitives, 1474-1481, (2014)
[16] Kaelbling, L; Lozano-Perez, T, Hierarchical task and motion planning in the now, 1470-1477, (2011)
[17] Kloetzer, M; Belta, C, Dealing with nondeterminism in symbolic control, 287-300, (2008) · Zbl 1143.68488
[18] Koo, T; Sastry, S, Bisimulation based hierarchical system architecture for single-agent multi-modal systems, 281-293, (2002) · Zbl 1044.93502
[19] Kruger N, Piater J, Worgotter F, Geib C, Petrick R, Steedman M, Asfour T, Kraft D, Hommel B, Agostini A et al (2009) A formal definition of object-action complexes and examples at different levels of the processing hierarchy. Computer and Information Science, pp 1-39 · Zbl 1374.68322
[20] Leva A (2016) Reactive controller synthesis for mobile robotics. Master’s thesis, University of Kaiserslautern, Germany. Available at https://www.mpi-sws.org/tr/2017-001.pdf
[21] Mazo, J; Manuel, A; Tabuada, P, PESSOA Davitian A tool for embedded controller synthesis, 566-569, (2010)
[22] Pappas, G; Lafferriere, G; Sastry, S, Hierarchically consistent control systems, IEEE Trans Autom Control, 45, 1144-1160, (2000) · Zbl 0971.93004
[23] Raisch, J; Moor, T, Hierarchical hybrid control synthesis and its application to a multiproduct batch plant, 199-216, (2005) · Zbl 1124.93340
[24] Reps T, Horwitz S, Sagiv S (1995) Precise interprocedural dataflow analysis via graph reachability POPL 95. ACM, pp 49-61 · Zbl 1471.68131
[25] Schmidt, K; Moor, T; Perk, S, Nonblocking hierarchical control of decentralized discrete event systems, IEEE Trans Autom Control, 53, 2252-2265, (2008) · Zbl 1367.93373
[26] Srivastava, S; Fang, E; Riano, L; Chitnis, R; Russell, S; Abbeel, P, Combined task and motion planning through an extensible planner-independent interface layer, 639-646, (2014)
[27] Stock, S; Mansouri, M; Pecora, F; Hertzberg, J, Hierarchical hybrid planning in a mobile service robot, 309-315, (2015)
[28] Tabuada P (2009) Verification and control of hybrid systems - a symbolic approach, vol 1. Springer · Zbl 1195.93001
[29] Vasile, CI; Belta, C, Reactive sampling-based temporal logic path planning, 4310-4315, (2014)
[30] Walukiewicz, I, Pushdown processes: games and model checking, 62-74, (1996)
[31] Wolff, E; Topcu, U; Murray, R, Optimal control of non-deterministic systems for a computationally efficient fragment of temporal logic, 3197-3204, (2013)
[32] Wong, KW; Finucane, C; Kress-Gazit, H, Provably-correct robot control with ltlmop, ompl and ros, 2073-2073, (2013)
[33] Wongpiromsarn, T; Topcu, U; Murray, R, Automatic synthesis of robust embedded control software, (2010)
[34] Wongpiromsarn, T; Topcu, U; Ozay, N; Xu, H; Murray, R, Tulip: a software toolbox for receding horizon temporal logic planning, 313-314, (2011)
[35] Wongpiromsarn, T; Topcu, U; Murray, R, Receding horizon temporal logic planning, IEEE Trans Autom Control, 57, 2817-2830, (2012) · Zbl 1360.68605
[36] Zielonka, W, Infinite games on finitely coloured graphs with applications to automata on infinite trees, Theor Comput Sci, 200, 135-183, (1998) · Zbl 0915.68120
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.