LTLf+ 의무 속성에 대한 심볼릭 합성

Symbolic Synthesis for LTLf+ Obligations

본 연구에서는 무한 트레이스를 표현하는 LTLfp의 확장인 LTLfp로 표현된 의무 속성에 대한 합성을 연구합니다. 의무 속성은 안전 속성과 보장(공안전) 속성의 양의 부울 조합으로 구성되며, 이는 만나(Manna)와 프누엘리(Pnueli)가 제안한 시간 계층 구조의 두 번째 레벨에 해당합니다. 의무 속성은 무한 트레이스에 대해 표현되지만, LTLfp와 마찬가지로 대부분의 단순성을 유지합니다. 특히, 본 연구에서는 의무 속성이 트레이스 접두사에 대한 기본 LTLfp 속성의 심볼릭 결정적 약한 오토마타(DWA)로 변환될 수 있음을 보여줍니다. DWA는 부울 닫힘 및 다항 시간 최소화와 같은 DFA의 많은 매력적인 알고리즘적 특징을 상속합니다. 또한, LTLfp 의무 속성에 대한 합성은 이론적으로 매우 효율적이며, DWA가 구성되면 선형 시간 내에 해결될 수 있습니다. 본 연구에서는 의무 속성 합성에 발생하는 DWA 게임을 해결하기 위한 여러 심볼릭 알고리즘을 조사하고, 실험적으로 그 효과를 평가합니다. 전반적으로, 본 연구 결과는 LTLfp 의무 속성에 대한 합성이 LTLfp 합성과 거의 동일한 효과를 낼 수 있음을 시사합니다.

We study synthesis for obligation properties expressed in LTLfp, the extension of LTLf to infinite traces. Obligation properties are positive Boolean combinations of safety and guarantee (co-safety) properties and form the second level of the temporal hierarchy of Manna and Pnueli. Although obligation properties are expressed over infinite traces, they retain most of the simplicity of LTLf. In particular, we show that they admit a translation into symbolically represented deterministic weak automata (DWA) obtained directly from the symbolic deterministic finite automata (DFA) for the underlying LTLf properties on trace prefixes. DWA inherit many of the attractive algorithmic features of DFA, including Boolean closure and polynomial-time minimization. Moreover, we show that synthesis for LTLfp obligation properties is theoretically highly efficient - solvable in linear time once the DWA is constructed. We investigate several symbolic algorithms for solving DWA games that arise in the synthesis of obligation properties and evaluate their effectiveness experimentally. Overall, the results indicate that synthesis for LTLfp obligation properties can be performed with virtually the same effectiveness as LTLf synthesis.