Analysis

Unsynthesizable Specifications

When controller synthesis fails, the specification is called unsynthesizable. Unsynthesizable specifications are either unsatisfiable, in which case the robot cannot succeed no matter what happens in the environment (e.g., if the task requires patrolling a disconnected workspace), or unrealizable, in which case there exists at least one environment that can prevent the desired behavior (e.g., if in the above task, the environment can disconnect an otherwise connected workspace, such as by closing a door).

In either case, the robot can fail in one of two ways: either it ends up in a state from which it has no valid moves (termed deadlock), or the robot is able to change its state infinitely, but one of its goals is unreachable without violating the specified safety requirements (termed livelock).

For unsynthesizable specifications, LTLMoP provides feedback by highlighting the sentences of the specification that contribute to the failure. An initial analysis determines whether the problem is deadlock or livelock, and whether it is caused by the portion of the specification that describes the desired robot behaviour, or the environment assumptions.

In the case of unsynthesizability caused by the specified behaviour, an additional refinement of the feedback identiies unsynthesizable cores – minimal subsets of the desired robot behavior that cause it to be unsatisfiable or unrealizable.