Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States

摘要

As robotic systems get more complex, logic specifications assist in precisely specifying desired behavior for a system and constructing controllers that provably guarantee satisfaction of the specification. In our work, we focus on reactive synthesis from temporal logic specifications. This involves reasoning about all admissible behaviors for the environment and synthesizing a policy for the controlled agent. This makes the algorithms for synthesis difficult to scale and synthesis can be prohibitively expensive when applied to problems with large state spaces.