Analysis

Unsynthesizable Specifications

When controller synthesis fails, the specification is called unsynthesizable. Unsynthesizable specifications are either:

• unsatisfiable: the robot cannot succeed no matter what happens in the environment (e.g., if the task requires patrolling a disconnected workspace), or
• unrealizable: 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).

Types of Failure

In either case, the robot can fail in one of two ways:

• it ends up in a state from which it has no valid moves (termed deadlock)
• it is able to change its state infinitely, but one of its goals is unreachable without violating the specified safety requirements (termed livelock)

Feedback

• 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.

Cores

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

TODO: screenshots TODO(?): SLURP feedback