Act for Your Duties but Maintain Your Rights
This work addresses the need for more flexible agent behavior in automated synthesis, though it is incremental as it builds on existing LTLf synthesis methods.
The paper tackles the problem of synthesizing strategies for intelligent agents that must fulfill mandatory duties while optionally maintaining rights, using LTLf specifications. It shows that incorporating rights does not substantially increase synthesis difficulty but requires a more sophisticated solution concept.
Most of the synthesis literature has focused on studying how to synthesize a strategy to fulfill a task. This task is a duty for the agent. In this paper, we argue that intelligent agents should also be equipped with rights, that is, tasks that the agent itself can choose to fulfill (e.g., the right of recharging the battery). The agent should be able to maintain these rights while acting for its duties. We study this issue in the context of LTLf synthesis: we give duties and rights in terms of LTLf specifications, and synthesize a suitable strategy to achieve the duties that can be modified on-the-fly to achieve also the rights, if the agent chooses to do so. We show that handling rights does not make synthesis substantially more difficult, although it requires a more sophisticated solution concept than standard LTLf synthesis. We also extend our results to the case in which further duties and rights are given to the agent while already executing.