{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T07:38:27Z","timestamp":1723016307509},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,9]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.24963\/kr.2021\/23","type":"proceedings-article","created":{"date-parts":[[2021,10,11]],"date-time":"2021-10-11T16:45:56Z","timestamp":1633970756000},"page":"237-246","source":"Crossref","is-referenced-by-count":1,"title":["Synthesis with Mandatory Stop Actions"],"prefix":"10.24963","author":[{"given":"Giuseppe","family":"De Giacomo","sequence":"first","affiliation":[{"name":"Sapienza University of Rome, Rome, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonio","family":"Di Stasio","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Rome, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Perelli","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Rome, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shufang","family":"Zhu","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Rome, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"number":"18","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","Sea AI Lab","Potassco Solutions","European Association for Artificial Intelligence"],"acronym":"KR-2021","name":"18th International Conference on Principles of Knowledge Representation and Reasoning {KR-2021}","start":{"date-parts":[[2020,11,12]]},"theme":"Artificial Intelligence","location":"Hanoii, Vietnam","end":{"date-parts":[[2021,11,18]]}},"container-title":["Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2021,10,11]],"date-time":"2021-10-11T16:46:10Z","timestamp":1633970770000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2021\/23"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2021,9]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2021\/23","relation":{},"subject":[],"published":{"date-parts":[[2021,9]]}}}