論文の概要: Symbolic Synthesis for LTLf+ Obligations
- arxiv url: http://arxiv.org/abs/2604.18532v1
- Date: Mon, 20 Apr 2026 17:27:28 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-21 21:52:53.017772
- Title: Symbolic Synthesis for LTLf+ Obligations
- Title（参考訳）: シンボリックなLTLf+の合成
- Authors: Giuseppe De Giacomo, Christian Hagemeier, Daniel Hausmann, Nir Piterman,
- Abstract要約: 合成 forfp の配当特性は理論的に高効率であり、線形時間で解けることを示す。
義務特性の合成において生じるDWAゲームを解決するためのいくつかのシンボリックアルゴリズムについて検討する。
- 参考スコア（独自算出の注目度）: 18.311321898495176
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract（参考訳）: 無限トレースへのLTLfの拡張であるLTLfpで表される義務特性の合成について検討する。
オブリグレーション特性は安全性と保証(コ・セーフティ)特性の正のブール結合であり、マンナとプヌエリの時間的階層の第二のレベルを形成する。
義務性は無限のトレース上で表されるが、それらはLTLfの単純さの大部分を保っている。
特に,記号的決定論的有限オートマトン (DFA) から直接得られる記号的決定論的弱オートマトン (DWA) への翻訳を認めた。
DWAはブール閉包や多項式時間最小化など、DFAの魅力的なアルゴリズム的特徴の多くを継承する。
さらに,LTLfpの配当特性の合成は理論上極めて効率的であり,DWAが構築されると線形時間で解けることを示す。
義務特性の合成において生じるDWAゲームを解くためのいくつかのシンボリックアルゴリズムについて検討し,その有効性を実験的に評価する。
その結果,LTLfpの配当特性の合成は,LTLfの合成とほぼ同等の効率で行うことができた。
関連論文リスト
- Multi-Property Synthesis [69.79949693440426]
複数の特性を持つ合成について研究し、全ての特性を満たすことは不可能かもしれない。
プロパティのサブセットを列挙する代わりに、製品ゲーム状態とそれらから実現可能なゴールセットの関係を1つの固定点計算で計算する。
論文 参考訳（メタデータ） (2026-01-15T18:18:33Z) - LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces [44.35335751462176]
オートマチックf+/PPLTL+のためのDFAベースの合成技術について述べる。
PPLTL+の表現力は2EXPTIME完全ではなくEXPTIME完全であることを示す。
論文 参考訳（メタデータ） (2024-11-14T11:17:06Z) - On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts [20.14001970300658]
トップダウン決定論的オートマトン構築に基づく有限トレース(LTLf)上での線形時間論理のオンザフライフレームワークを提案する。
論文 参考訳（メタデータ） (2024-08-14T06:52:58Z) - Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis [1.1797787239802762]
本稿では,古典的リアクティブハンドル(命題)を仕様言語として,時間論理仕様から正しいコントローラを生成する方法を示す。
また,制御器が常に最小の安全値を提供するために出力を最適化できるという意味で応答が可能であることを示す。
論文 参考訳（メタデータ） (2024-07-12T15:23:27Z) - A first-order logic characterization of safety and co-safety languages [63.29821624186913]
有限の接頭辞が、ある単語が言語に属していないか、属していないかを確立するのに十分である安全で共同安全な言語は、モデル検査や反応合成のような問題の複雑さを下げる上で重要な役割を果たす。
本稿では,安全性とコセーフティ言語に関して,FO-TLOの断片であるSafetyFOと,その二重コセーフティについて述べる。
論文 参考訳（メタデータ） (2022-09-06T09:00:38Z) - A Normal Form Characterization for Efficient Boolean Skolem Function
Synthesis [2.093287944284448]
本稿では,通常の合成をトラクタブルに特徴づけるSAUNFという表現形式を提案する。
AIの問題の文脈で使用されるBDDやDNNFのような確立された通常の形式よりも指数関数的に簡潔であり、SynNNFのような他のより最近提案された形式を厳密に推定する。
論文 参考訳（メタデータ） (2021-04-29T04:16:41Z) - LTLf Synthesis on Probabilistic Systems [0.0]
合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。
有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。
本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
論文 参考訳（メタデータ） (2020-09-23T01:26:47Z) - Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
本稿では,リアプノフ関数の自動合成法を提案する。
我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。
提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
論文 参考訳（メタデータ） (2020-03-19T17:21:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。