論文の概要: 3vLTL: A Tool to Generate Automata for Three-valued LTL

• arxiv url: http://arxiv.org/abs/2311.09787v1
• Date: Thu, 16 Nov 2023 11:04:38 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-17 14:41:50.772229
• Title: 3vLTL: A Tool to Generate Automata for Three-valued LTL
• Title（参考訳）: 3vltl:3値ltlのautomattaを生成するツール
• Authors: Francesco Belardinelli (Imperial College London), Angelo Ferrando (University of Genoa), Vadim Malvone (Telecom Paris)
• Abstract要約: 線形時間時間時間論理(LTL)の式からBuchi Automaticaを生成するツールである3vLTLを提案する。 提案手法は,選択した真理値を式に割り当てるすべての単語を受理するBuchiオートマトンを生成する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Multi-valued logics have a long tradition in the literature on system verification, including run-time verification. However, comparatively fewer model-checking tools have been developed for multi-valued specification languages. We present 3vLTL, a tool to generate Buchi automata from formulas in Linear-time Temporal Logic (LTL) interpreted on a three-valued semantics. Given an LTL formula, a set of atomic propositions as the alphabet for the automaton, and a truth value, our procedure generates a Buchi automaton that accepts all the words that assign the chosen truth value to the LTL formula. Given the particular type of the output of the tool, it can also be seamlessly processed by third-party libraries in a natural way. That is, the Buchi automaton can then be used in the context of formal verification to check whether an LTL formula is true, false, or undefined on a given model.
• Abstract（参考訳）: 多値論理は、実行時検証を含むシステム検証に関する文献において長い伝統を持っている。 しかし、多値仕様言語向けの比較的少ないモデルチェックツールが開発されている。 線形時間時間時間論理(LTL)の式からBuchi Automaticaを生成するツールである3vLTLを3値意味論で解釈する。 ltl公式と、オートマトンのためのアルファベットとしての原子命題の集合と真理値が与えられたとき、この手順は、選択された真理値をltl公式に割り当てる全ての単語を受け入れるbuchiオートマトンを生成する。 ツールの出力の特定のタイプを考えると、自然な方法でサードパーティのライブラリによってシームレスに処理することもできる。 すなわち、buchiオートマトンは形式的検証の文脈において、与えられたモデル上で ltl の公式が真であるか偽であるか未定義であるかをチェックするために用いられる。

関連論文リスト

• CoT-TL: Low-Resource Temporal Knowledge Representation of Planning Instructions Using Chain-of-Thought Reasoning [0.0]
  CoT-TLは、自然言語仕様を表現に変換するためのデータ効率のよいインコンテキスト学習フレームワークである。 CoT-TLは、ローデータシナリオで3つの多様なデータセット間で最先端の精度を達成する。
  論文  参考訳（メタデータ） (2024-10-21T17:10:43Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。 AutoIFは命令追従データ品質の検証をコード検証に変換する。
  論文  参考訳（メタデータ） (2024-06-19T13:29:53Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification [6.091096843566857]
  本稿では、自然言語コマンドから、人間ラベルの訓練データに制限のある仕様への変換を学習ベースで行う手法を提案する。 これは、人間のラベル付きデータセットを必要とする既存の自然言語から翻訳者への変換とは対照的である。 自然言語コマンドを75%の精度で翻訳できることを示す。
  論文  参考訳（メタデータ） (2023-03-09T00:09:58Z)
• Automatic Label Sequence Generation for Prompting Sequence-to-sequence Models [105.4590533269863]
  完全自動プロンプト方式であるAutoSeqを提案する。 我々はシーケンス・ツー・シーケンス・モデルに自然言語プロンプトを採用する。 本手法は,数ショット学習におけるシーケンス・ツー・シーケンスモデルの可能性を明らかにする。
  論文  参考訳（メタデータ） (2022-09-20T01:35:04Z)
• Neuro-Symbolic Language Modeling with Automaton-augmented Retrieval [129.25914272977542]
  RetoMatonはデータストア上に構築された重み付き有限オートマトンである。 LM推論と並行して、このオートマトンを推論時にトラバースすることは、その複雑さを減少させる。
  論文  参考訳（メタデータ） (2022-01-28T21:38:56Z)
• Automata for dynamic answer set solving: Preliminary report [0.0]
  本稿では,動的論理から言語構造を記述したAnswer Set Programming(ASP)の拡張で表現される時間的制約を実装する方法について検討する。 その考え方は、動的制約を、元の制約の満足度を強制する論理プログラムの言葉で表現されたオートマトンに変換することである。
  論文  参考訳（メタデータ） (2021-09-04T03:58:12Z)
• Induction and Exploitation of Subgoal Automata for Reinforcement Learning [75.55324974788475]
  本稿では,Regressed Learning (RL)タスクにおけるサブゴールの学習と活用のためのISAを提案する。 ISAは、タスクのサブゴールによってエッジがラベル付けされたオートマトンであるサブゴールオートマトンを誘導することで強化学習をインターリーブする。 サブゴールオートマトンはまた、タスクの完了を示す状態と、タスクが成功せずに完了したことを示す状態の2つの特別な状態で構成されている。
  論文  参考訳（メタデータ） (2020-09-08T16:42:55Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。