Controller Synthesis for Mode-Target Games

摘要

Cyber-Physical Systems (CPS) are notoriously difficult to verify due to the intricate interactions between the cyber and the physical components. To address this difficulty, several researchers have argued that the synthesis paradigm is better suited to ensure the correct operation of CPS than the verification paradigm. The key insight of synthesis is that design should be constrained so that resulting systems are easily verified and, ideally, synthesis algorithms should directly provide a proof of correctness.In this paper we present a Linear Temporal Logic fragment inspired by specifications that frequently occur in control applications where we have a set of modes and corresponding targets to be reached for each mode. The synthesis problem for this fragment is formulated as a mode-target game and we show that these games can be solved in polynomial time by providing two embeddings of mode-target games into Generalized Reactivity(1) (GR(1)) games. While solving GR(1) games requires O(mnN2) symbolic steps when we have m assumptions, n guarantees, and a game graph with N states, mode-target games can be solved in O(nN2) symbolic steps when we have n modes and a game graph with N states. These embeddings, however, do not make full use of the specificity of mode-target games. For this reason we investigate in this paper a solution to mode-target games that does not rely on GR(1) embeddings. The resulting algorithm has the same worst case time complexity and we illustrate through experimental results the extent to which it improves upon the algorithms obtained via GR(1) embeddings. In doing so, we highlight the commonalities between mode-target games and GR(1) games while providing additional insight into the solution of GR(1) games.