論文の概要: A Sahlqvist-style Correspondence Theorem for Linear-time Temporal Logic
- arxiv url: http://arxiv.org/abs/2206.05973v1
- Date: Mon, 13 Jun 2022 08:36:13 GMT
- ステータス: 処理完了
- システム内更新日: 2022-06-15 00:06:18.208101
- Title: A Sahlqvist-style Correspondence Theorem for Linear-time Temporal Logic
- Title(参考訳): 線形時間時相論理に対するsahlqvist型対応定理
- Authors: Rui Li, Francesco Belardinelli
- Abstract要約: 線形時間時間時間論理(LTL)のためのShlqvist型対応定理を開発する。
モーダル作用素 F, G, X, U を用いて構築されたサルクヴィスト公式の有意なクラスを同定する。
本論文の主な成果は、一階言語で定義可能なフレーム条件に対するソルクヴィスト公式の対応性を証明することである。
- 参考スコア(独自算出の注目度): 10.029813712651471
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The language of modal logic is capable of expressing first-order conditions
on Kripke frames. The classic result by Henrik Sahlqvist identifies a
significant class of modal formulas for which first-order conditions -- or
Sahlqvist correspondents -- can be find in an effective, algorithmic way.
Recent works have successfully extended this classic result to more complex
modal languages. In this paper, we pursue a similar line and develop a
Sahlqvist-style correspondence theorem for Linear-time Temporal Logic (LTL),
which is one of the most widely used formal languages for temporal
specification. LTL extends the syntax of basic modal logic with dedicated
temporal operators Next X and Until U . As a result, the complexity of the
class of formulas that have first-order correspondents also increases
accordingly. In this paper, we identify a significant class of LTL Sahlqvist
formulas built by using modal operators F , G, X, and U . The main result of
this paper is to prove the correspondence of LTL Sahlqvist formulas to frame
conditions that are definable in first-order language.
- Abstract(参考訳): モーダル論理の言語はクリプキフレーム上の一階条件を表現することができる。
Henrik Sahlqvist による古典的な結果は、一階条件 (あるいは Sahlqvist 対応式) が効果的でアルゴリズム的な方法で発見できる、重要なモーダル公式のクラスを特定できる。
最近の作品は、この古典的な結果をより複雑なモーダル言語に拡張することに成功している。
本稿では,線形時時時論理 (LTL) に対する類似の行を追求し,時相仕様のための最も広く使われている形式言語の一つである Sahlqvist 形式の対応定理を開発する。
LTLは、基本的なモーダル論理の構文を拡張し、専用のテンポラル演算子Next X と until U を持つ。
その結果、一階の対応式を持つ公式のクラスの複雑さも、それに応じて増加する。
本稿では, モーダル作用素 F , G, X, U を用いて構築した LTL Sahlqvist 公式の有意なクラスを同定する。
本論文の主な結果は、一階言語で定義可能なフレーム条件に対するltl sahlqvist公式の対応を証明することである。
関連論文リスト
- LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳(メタデータ) (2023-10-23T17:58:40Z) - Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。
有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
論文 参考訳(メタデータ) (2023-07-31T17:02:23Z) - On Loop Formulas with Variables [2.1955512452222696]
最近、フェラーリス、リー、リフシッツはグラウンド化に言及しない安定モデルの新たな定義を提案した。
我々は、Chen, Lin, Wang, Zhang による変数を持つループ公式のアイデアとの関係を示す。
論理プログラムの構文を拡張して、明示的な量化を許容し、その意味論を安定モデルの新しい言語のサブクラスとして定義する。
論文 参考訳(メタデータ) (2023-07-15T06:20:43Z) - The Alternating-Time \mu-Calculus With Disjunctive Explicit Strategies [1.7725414095035827]
同時ゲーム構造におけるエージェントの連立の戦略能力について検討する。
論理の重要な要素は、あるエージェントの連立が与えられた目標を強制するための共同戦略を持つことを示す経路定量化器である。
我々は, ATLES を固定点演算子と戦略解離で拡張し, 明示的な戦略で時相の $mu$-calculus に到達する。
論文 参考訳(メタデータ) (2023-05-30T07:16:59Z) - Lexinvariant Language Models [84.2829117441298]
離散語彙記号から連続ベクトルへの写像であるトークン埋め込みは、任意の言語モデル(LM)の中心にある
我々は、語彙記号に不変であり、したがって実際に固定トークン埋め込みを必要としないテクスチトレキシン変種モデルについて研究する。
十分長い文脈を条件として,レキシン変項LMは標準言語モデルに匹敵する難易度が得られることを示す。
論文 参考訳(メタデータ) (2023-05-24T19:10:46Z) - Structural generalization is hard for sequence-to-sequence models [85.0087839979613]
シーケンス・ツー・シーケンス(seq2seq)モデルは、多くのNLPタスクで成功している。
構成一般化に関する最近の研究は、セq2seqモデルは訓練で見られなかった言語構造への一般化において非常に低い精度を達成することを示した。
論文 参考訳(メタデータ) (2022-10-24T09:03:03Z) - A first-order logic characterization of safety and co-safety languages [63.29821624186913]
有限の接頭辞が、ある単語が言語に属していないか、属していないかを確立するのに十分である安全で共同安全な言語は、モデル検査や反応合成のような問題の複雑さを下げる上で重要な役割を果たす。
本稿では,安全性とコセーフティ言語に関して,FO-TLOの断片であるSafetyFOと,その二重コセーフティについて述べる。
論文 参考訳(メタデータ) (2022-09-06T09:00:38Z) - Understanding Robust Generalization in Learning Regular Languages [85.95124524975202]
我々は、リカレントニューラルネットワークを用いて正規言語を学習する文脈における堅牢な一般化について研究する。
この問題に対処するための構成戦略を提案する。
構成戦略がエンド・ツー・エンド戦略よりもはるかに優れていることを理論的に証明する。
論文 参考訳(メタデータ) (2022-02-20T02:50:09Z) - Temporal Answer Set Programming [3.263632801414296]
本稿では,その知識表現と宣言的問題解決への応用の観点から,時間論理プログラミングの概要を述べる。
本研究は,TEL(Temporal Equilibrium Logic)と呼ばれる非単調な形式論の最近の成果に焦点を当てる。
第2部では,ASP.NET に近い時間論理プログラムと呼ばれる構文的断片を定義し,この問題が解決器 TEINGO の構築においてどのように活用されたかを説明する。
論文 参考訳(メタデータ) (2020-09-14T16:13:36Z) - A Formal Language Approach to Explaining RNNs [6.624726878647541]
本稿では、線形時間論理(LTL)と呼ばれる形式記述言語を用いて、リカレントニューラルネットワーク(RNN)の意思決定を説明するためのフレームワークであるLEXRを提案する。
LEXRの説明は、RNNから決定論的有限オートマトンを抽出する最近のアルゴリズムで生成されるものよりも正確で理解しやすい。
論文 参考訳(メタデータ) (2020-06-12T16:17:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。