We study the impact of the need for the agent to obligatorily instruct the action stop in her strategies. More specifically we consider synthesis (i.e., planning) for LTLf goals under LTL environment specifications in the case the agent must mandatorily stop at a certain point. We show that this obligation makes it impossible to exploit the liveness part of the LTL environment specifications to achieve her goal, effectively reducing the environment specifications to their safety part only. This has a deep impact on the efficiency of solving the synthesis, which can sidestep handling Buchi determinization associated to LTL synthesis, in favor of finite-state automata manipulation as in LTLf synthesis. Next, we add to the agent goal, expressed in LTLf, a safety goal, expressed in LTL. Safety goals must hold forever, even when the agent stops, since the environment can still continue its evolution. Hence the agent, before stopping, must ensure that her safety goal will be maintained even after she stops. To do synthesis in this case, we devise an effective approach that mixes a synthesis technique based on finite-state automata (as in the case of LTLf goals) and model-checking of nondeterministic Buchi automata. In this way, again, we sidestep Buchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.
On the model checking of finite state transducers over semigroups