점진적 LTLf 합성

Incremental LTLf Synthesis

본 논문에서는 실행 중에 목표가 점진적으로 주어지는 반응형 합성의 한 형태인 점진적 LTLf 합성에 대해 연구합니다. 즉, 에이전트는 특정 목표에 대한 전략을 이미 실행하고 있을 때 새로운 목표를 받으면, 에이전트는 현재 전략을 포기하고 초기 목표와 새로운 목표를 모두 만족하는 새로운 전략을 현재 시점부터 합성해야 합니다. 본 논문에서는 점진적 합성 문제를 형식적으로 정의하고, 그 해결 방안을 연구합니다. 오토마타 기반 합성을 수행하는 동안 생성되는 보조 데이터 구조를 활용하여 여러 LTLf 목표에 대한 효율적인 점진적 합성을 수행하는 기법을 제안합니다. 또한, LTLf 공식의 점진적 확장을 기반으로 하는 대체 해결 기법을 고려합니다. 공식 확장이 원래 공식보다 지수적으로 더 큰 공식을 생성할 수 있다는 사실에도 불구하고, 최소 오토마타의 크기는 원래 공식의 크기로 제한됨을 보입니다. 반면, 공식 확장을 기반으로 하는 해결 기법이, 즉 새로운 목표가 도착할 때마다 확장된 LTLf 공식의 오토마타를 처음부터 계산하는 방식으로 구현될 경우, 실험적으로 경쟁력이 없음을 보여줍니다.

In this paper, we study incremental LTLf synthesis -- a form of reactive synthesis where the goals are given incrementally while in execution. In other words, the protagonist agent is already executing a strategy for a certain goal when it receives a new goal: at this point, the agent has to abandon the current strategy and synthesize a new strategy still fulfilling the original goal, which was given at the beginning, as well as the new goal, starting from the current instant. In this paper, we formally define the problem of incremental synthesis and study its solution. We propose a solution technique that efficiently performs incremental synthesis for multiple LTLf goals by leveraging auxiliary data structures constructed during automata-based synthesis. We also consider an alternative solution technique based on LTLf formula progression. We show that, in spite of the fact that formula progression can generate formulas that are exponentially larger than the original ones, their minimal automata remain bounded in size by that of the original formula. On the other hand, we show experimentally that, if implemented naively, i.e., by actually computing the automaton of the progressed LTLf formulas from scratch every time a new goal arrives, the solution based on formula progression is not competitive.