論文の概要: A first-order logic characterization of safety and co-safety languages
- arxiv url: http://arxiv.org/abs/2209.02307v5
- Date: Wed, 9 Aug 2023 07:59:56 GMT
- ステータス: 処理完了
- システム内更新日: 2023-08-10 18:30:22.838916
- Title: A first-order logic characterization of safety and co-safety languages
- Title（参考訳）: 安全・共安全言語の一階述語論理
- Authors: Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari,
Stefano Tonetta
- Abstract要約: 有限の接頭辞が、ある単語が言語に属していないか、属していないかを確立するのに十分である安全で共同安全な言語は、モデル検査や反応合成のような問題の複雑さを下げる上で重要な役割を果たす。
本稿では,安全性とコセーフティ言語に関して,FO-TLOの断片であるSafetyFOと,その二重コセーフティについて述べる。
- 参考スコア（独自算出の注目度）: 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 Linear Orders
(FO-TLO). 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
FO-TLO, 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 は反自由オメガオートマタ、星のないオメガ正規表現、(カンプの定理により)一階線形順序理論(FO-TLO)と等価である。
安全性(safety)とコセーフティ(co-safety)言語は、単語がそれぞれ言語に属さないか属さないかを確立するために有限プレフィックスが十分であり、モデル検査やltlのリアクティブ合成のような問題の複雑さを低下させる上で重要な役割を果たす。
SafetyLTL (resp., coSafetyLTL) はLTLの断片であり、安全(resp., co-safety)言語のみを認識する普遍的(resp., existential)時間的モダリティのみを許容する。
この論文の主な貢献は、safetyfoと呼ばれるfo-tloの断片と、ltl-definable safetyとco-safety languageに関して表現的に完結した2つのcosafetyfoの導入である。
我々は,これらがそれぞれSafetyLTLとcoSafetyLTLを正確に特徴付けることを証明し,その結果がカンプの定理に一致することを証明し,一階言語の観点からLTLの特徴付け(フラグメント)をより明確にする。
さらに、ltlで定義可能な安全言語がsafetyltlでも定義可能であることを直接的でコンパクトで自己完結した証明を与える。
副産物として,有限語および無限語で解釈された,明日の弱作用素SafetyLTLの表現力に関する興味深い結果が得られる。
さらに、有限語を解釈すると、明日の(弱明日)演算子を欠いたsafetyltl (resp. cosafetyltl) が有限語上のltlの安全(resp., co-safety)フラグメントをキャプチャする。
関連論文リスト
- garak: A Framework for Security Probing Large Language Models [16.305837349514505]
garakは、ターゲットとするLarge Language Models(LLM)の脆弱性を発見し、特定するために使用できるフレームワークである。
フレームワークのアウトプットは、ターゲットモデルの弱点を記述し、ユニークなコンテキストで脆弱性を構成するものについての情報的な議論に寄与する。
論文 参考訳（メタデータ） (2024-06-16T18:18:43Z) - Towards Comprehensive and Efficient Post Safety Alignment of Large Language Models via Safety Patching [77.36097118561057]
textscSafePatchingは包括的で効率的なPSAのための新しいフレームワークである。
textscSafePatchingはベースラインメソッドよりも包括的で効率的なPSAを実現する。
論文 参考訳（メタデータ） (2024-05-22T16:51:07Z) - A Framework for Real-time Safeguarding the Text Generation of Large Language Model [12.683042228674694]
大規模言語モデル(LLM)は、非常に高度な自然言語処理(NLP)タスクを持つ。
有害なコンテンツを発生させる傾向にあるため、倫理的・社会的リスクが生じる。
LLMテキスト生成をリアルタイムに保護する軽量フレームワークであるLLMSafeGuardを提案する。
論文 参考訳（メタデータ） (2024-04-29T18:40:01Z) - CodeAttack: Revealing Safety Generalization Challenges of Large Language Models via Code Completion [117.178835165855]
本稿では,自然言語入力をコード入力に変換するフレームワークであるCodeAttackを紹介する。
我々の研究は、コード入力に対するこれらのモデルの新たな、普遍的な安全性の脆弱性を明らかにした。
CodeAttackと自然言語の分布ギャップが大きくなると、安全性の一般化が弱くなる。
論文 参考訳（メタデータ） (2024-03-12T17:55:38Z) - 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) - Trojaning Language Models for Fun and Profit [53.45727748224679]
TROJAN-LMは、悪質に製作されたLMがホストNLPシステムを故障させる新しいタイプのトロイの木馬攻撃である。
セキュリティクリティカルなNLPタスクにおいて、3つの最先端のLMを実証的に研究することにより、TROJAN-LMが以下の特性を持つことを示す。
論文 参考訳（メタデータ） (2020-08-01T18:22:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。