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 Büchi 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 Büchi automata. In this way, again, we sidestep Büchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.
Synthesis with mandatory stop actions / DE GIACOMO, Giuseppe; DI STASIO, Antonio; Perelli, Giuseppe; Zhu, Shufang. - (2021), pp. 237-246. (Intervento presentato al convegno International Conference on the Principles of Knowledge Representation and Reasoning tenutosi a Online event) [10.24963/kr.2021/23].
Synthesis with mandatory stop actions
Giuseppe De Giacomo;Antonio Di Stasio;Giuseppe Perelli;Shufang Zhu
2021
Abstract
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 Büchi 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 Büchi automata. In this way, again, we sidestep Büchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.File | Dimensione | Formato | |
---|---|---|---|
DeGiacomo_Synthesis_2021.pdf
accesso aperto
Note: https://doi.org/10.24963/kr.2021/23
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
199.99 kB
Formato
Adobe PDF
|
199.99 kB | Adobe PDF |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.