論文の概要: 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 の公式が真であるか偽であるか未定義であるかをチェックするために用いられる。
関連論文リスト
- Fine-Tuning and Prompt Engineering for Large Language Models-based Code Review Automation [4.941630596191807]
コードレビュー自動化にLLM(Large Language Models)を利用する場合、ファインチューニングとプロンプトが一般的なアプローチである。
LLMベースのコードレビュー自動化では、モデルファインチューニングと推論技術(ゼロショット学習、少数ショット学習、ペルソナ)を使用します。
その結果、ゼロショット学習によるGPT-3.5は、Guoらのアプローチよりも73.17%-74.23%高いEMが得られることがわかった。
論文 参考訳(メタデータ) (2024-02-01T03:10:26Z) - ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation [10.503097140635374]
ChIRAAGはOpenAI GPT4をベースとして、自然言語仕様からSVAアサーションを生成する。
ChIRAAGは、設計仕様を標準化されたフォーマットに体系的に分解する。
LLM生成したアサーションを検証・検証するためのテストベンチを開発した。
論文 参考訳(メタデータ) (2024-01-31T12:41:27Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳(メタデータ) (2023-11-15T14:41:57Z) - Large Language Model-Aware In-Context Learning for Code Generation [75.68709482932903]
大規模言語モデル(LLM)は、コード生成において印象的なコンテキスト内学習(ICL)能力を示している。
コード生成のためのLAIL (LLM-Aware In-context Learning) という新しい学習ベース選択手法を提案する。
論文 参考訳(メタデータ) (2023-10-15T06:12:58Z) - AnnoLLM: Making Large Language Models to Be Better Crowdsourced Annotators [98.11286353828525]
GPT-3.5シリーズのモデルは、様々なNLPタスクにまたがる顕著な少数ショットとゼロショットの能力を示している。
本稿では,2段階のアプローチを取り入れたAnnoLLMを提案する。
我々はAnnoLLMを用いた対話型情報検索データセットを構築した。
論文 参考訳(メタデータ) (2023-03-29T17:03:21Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。