論文の概要: A first-order logic characterization of safety and co-safety languages
- arxiv url: http://arxiv.org/abs/2209.02307v1
- Date: Tue, 6 Sep 2022 09:00:38 GMT
- ステータス: 処理完了
- システム内更新日: 2022-09-07 14:51:09.687548
- Title: A first-order logic characterization of safety and co-safety languages
- Title(参考訳): 安全・共安全言語の一階述語論理
- Authors: Alessandro Cimatti and Luca Geatti and Nicola Gigante and Angelo
Montanari and Stefano Tonetta
- Abstract要約: 安全性とコセーフティ言語は、モデルチェックやリアクティブ合成といった問題の複雑さを低減する上で重要な役割を担います。
本稿では,セーフティーフォ (SafetyFO) と呼ばれるS1S[FO) の断片と,その2つのコセーフティフォ (coSafetyFO) について紹介する。
- 参考スコア(独自算出の注目度): 63.29821624186913
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Linear Temporal Logic (LTL) is one of the most popular temporal logics, that
comes into play in a variety of branches of computer science. Among the various
reasons of its widespread use there are its strong foundational properties: LTL
is equivalent to counter-free omega-automata, to star-free omega-regular
expressions, and (by Kamp's theorem) to the first-order theory of one successor
(S1S[FO]). Safety and co-safety languages, where a finite prefix suffices to
establish whether a word does not belong or belongs to the language,
respectively, play a crucial role in lowering the complexity of problems like
model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL)
is a fragment of LTL where only universal (resp., existential) temporal
modalities are allowed, that recognises safety (resp., co-safety) languages
only.
The main contribution of this paper is the introduction of a fragment of
S1S[FO], called SafetyFO, and of its dual coSafetyFO, which are expressively
complete with respect to the LTL-definable safety and co-safety languages. We
prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a
result that joins Kamp's theorem, and provides a clearer view of the
characterization of (fragments of) LTL in terms of first-order languages. In
addition, it gives a direct, compact, and self-contained proof that any safety
language definable in LTL is definable in SafetyLTL as well. As a by-product,
we obtain some interesting results on the expressive power of the weak tomorrow
operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we
prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL)
devoid of the tomorrow (resp., weak tomorrow) operator captures the safety
(resp., co-safety) fragment of LTL over finite words.
- Abstract(参考訳): LTL(Linear Temporal Logic)は、コンピュータ科学の様々な分野において、最も一般的な時間論理の1つである。
LTL は反自由オメガオートマタ、星のないオメガ正規表現、そして(カンプの定理により)1つの後継者の1階理論(S1S[FO])と等価である。
安全性(safety)とコセーフティ(co-safety)言語は、単語がそれぞれ言語に属さないか属さないかを確立するために有限プレフィックスが十分であり、モデル検査やltlのリアクティブ合成のような問題の複雑さを低下させる上で重要な役割を果たす。
SafetyLTL (resp., coSafetyLTL) はLTLの断片であり、安全(resp., co-safety)言語のみを認識する普遍的(resp., existential)時間的モダリティのみを許容する。
この論文の主な貢献は、safetyfoと呼ばれるs1s[fo]の断片と、ltl-definable safetyとco-safety languageに関して表現的に完結したcosafetyfoの2つの断片の導入である。
我々は,これらがそれぞれSafetyLTLとcoSafetyLTLを正確に特徴付けることを証明し,その結果がカンプの定理に一致することを証明し,一階言語の観点からLTLの特徴付け(フラグメント)をより明確にする。
さらに、ltlで定義可能な安全言語がsafetyltlでも定義可能であることを直接的でコンパクトで自己完結した証明を与える。
副産物として,有限語および無限語で解釈された,明日の弱作用素SafetyLTLの表現力に関する興味深い結果が得られる。
さらに、有限語を解釈すると、明日の(弱明日)演算子を欠いたsafetyltl (resp. cosafetyltl) が有限語上のltlの安全(resp., co-safety)フラグメントをキャプチャする。
関連論文リスト
- Exploring Safety Generalization Challenges of Large Language Models via Code [126.80573601180411]
本稿では,自然言語入力をコード入力に変換するフレームワークであるCodeAttackを紹介する。
調査によると、CodeAttackは全モデルの80%以上の安全ガードレールを一貫してバイパスしている。
CodeAttackと自然言語の間の大きな分散ギャップは、安全性の一般化を弱める。
論文 参考訳(メタデータ) (2024-03-12T17:55:38Z) - ROSE Doesn't Do That: Boosting the Safety of Instruction-Tuned Large
Language Models with Reverse Prompt Contrastive Decoding [95.49128988683191]
本稿では,既存の命令調整LDMの安全性を高めるための簡易な手法であるROSE(Reverse prompt contrastive decoding)を提案する。
6つの安全性と2つの汎用タスクの実験から、ROSEは5種類の命令調整LDMに対して、一貫した、重要な安全性向上(+13.8%の安全性スコア)をもたらすだけでなく、LLMの汎用能力にも恩恵をもたらすことが示されている。
論文 参考訳(メタデータ) (2024-02-19T06:58:42Z) - LLM-FuncMapper: Function Identification for Interpreting Complex Clauses
in Building Codes via LLM [3.802984168589694]
LLM-FuncMapperは、様々な規制条項を解釈するために必要な事前定義された関数を特定するアプローチである。
ほぼ100%のコンピュータ処理可能な節をコンピュータ実行可能なコードとして解釈し表現することができる。
この研究は、複雑な規制条項を理解し解釈するためのLSMを導入する最初の試みである。
論文 参考訳(メタデータ) (2023-08-17T01:58:04Z) - Latent Jailbreak: A Benchmark for Evaluating Text Safety and Output
Robustness of Large Language Models [28.37026309925163]
大きな言語モデル(LLM)は人間の値と一致し、安全なテキストを生成するように設計されている。
以前のJailbreaking LLMのベンチマークでは、主にモデルの安全性の評価に焦点が当てられていた。
本稿では,LLMの安全性とロバスト性を両立させ,バランスの取れたアプローチの必要性を強調した。
論文 参考訳(メタデータ) (2023-07-17T13:49:52Z) - Red Teaming Language Model Detectors with Language Models [114.36392560711022]
大規模言語モデル(LLM)は、悪意のあるユーザによって悪用された場合、重大な安全性と倫理的リスクをもたらす。
近年,LLM生成テキストを検出し,LLMを保護するアルゴリズムが提案されている。
1) LLMの出力中の特定の単語を, 文脈が与えられたシノニムに置き換えること, 2) 生成者の書き方を変更するための指示プロンプトを自動で検索すること,である。
論文 参考訳(メタデータ) (2023-05-31T10:08:37Z) - Provable Adversarial Robustness for Fractional Lp Threat Models [136.79415677706612]
分数L_pの「ノルム」で区切られた攻撃はまだ十分に検討されていない。
いくつかの望ましい性質を持つ防衛法を提案する。
証明可能な(認証された)堅牢性を提供し、ImageNetにスケールし、(高い確率ではなく)決定論的保証を得る。
論文 参考訳(メタデータ) (2022-03-16T21:11:41Z) - LTLf Synthesis on Probabilistic Systems [0.0]
合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。
有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。
本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
論文 参考訳(メタデータ) (2020-09-23T01:26:47Z) - Trojaning Language Models for Fun and Profit [53.45727748224679]
TROJAN-LMは、悪質に製作されたLMがホストNLPシステムを故障させる新しいタイプのトロイの木馬攻撃である。
セキュリティクリティカルなNLPタスクにおいて、3つの最先端のLMを実証的に研究することにより、TROJAN-LMが以下の特性を持つことを示す。
論文 参考訳(メタデータ) (2020-08-01T18:22:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。