論文の概要: LTL under reductions with weaker conditions than stutter-invariance
- arxiv url: http://arxiv.org/abs/2111.03342v1
- Date: Fri, 5 Nov 2021 09:29:21 GMT
- ステータス: 処理完了
- システム内更新日: 2021-11-08 15:50:27.527005
- Title: LTL under reductions with weaker conditions than stutter-invariance
- Title(参考訳): スタッタ不変性より弱い条件下でのLTL
- Authors: Emmanuel Paviot-Adet, Denis Poitrenaud, Etienne Renault (LRDE), Yann
Thierry-Mieg
- Abstract要約: 我々は、スタッター感度よりも弱い性質について研究する。
ストラッター不感な言語では、単語にスタッターを加えて削除しても、その受け入れは変わらない。
その後、半決定手順を導入し、不感度特性を確実に証明したり、短めの非感度特性を否定する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Verification of properties expressed as-regular languages such as LTL can
benefit hugely from stutter-insensitivity, using a diverse set of reduction
strategies. However properties that are not stutter-insensitive, for instance
due to the use of the neXt operator of LTL or to some form of counting in the
logic, are not covered by these techniques in general. We propose in this paper
to study a weaker property than stutter-insensitivity. In a stutter insensitive
language both adding and removing stutter to a word does not change its
acceptance, any stuttering can be abstracted away; by decomposing this
equivalence relation into two implications we obtain weaker conditions. We
define a shortening insensitive language where any word that stutters less than
a word in the language must also belong to the language. A lengthening
insensitive language has the dual property. A semi-decision procedure is then
introduced to reliably prove shortening insensitive properties or deny
lengthening insensitive properties while working with a reduction of a system.
A reduction has the property that it can only shorten runs. Lipton's
transaction reductions or Petri net agglomerations are examples of eligible
structural reduction strategies. An implementation and experimental evidence is
provided showing most nonrandom properties sensitive to stutter are actually
shortening or lengthening insensitive. Performance of experiments on a large
(random) benchmark from the model-checking competition indicate that despite
being a semi-decision procedure, the approach can still improve state of the
art verification tools.
- Abstract(参考訳): ltlのような正規言語として表現される特性の検証は、様々な還元戦略を用いて、スタッター非感受性から大きな利益を得られる。
しかし、例えば LTL の NeXt 演算子の使用や論理学における何らかの数え方により、スタッター非感受性を持たない性質は、一般にこれらの手法によってカバーされない。
本稿では, スタッタ感度よりも弱い特性について検討する。
単語へのstutterの追加と削除の両方が受け付けを変えない頑固な非感受性言語では、任意のstutteringを抽象化することができ、この等価関係を2つの意味に分解することで、より弱い条件が得られる。
我々は、言語内の単語よりも短い単語も言語に属する必要があるという短大化非感受性言語を定義する。
延長不感な言語は二重性を持つ。
次に、半決定手順を導入し、システムの縮小に取り組みながら、無感性特性の短縮や無感性特性の延長の否定を確実に証明する。
削減には、実行の短縮しかできない特性がある。
リプトンの取引削減あるいはペトリネット集積は、許容される構造的削減戦略の例である。
ストッターに敏感なほとんどの非ランダム性は、実際には、非感受性の短縮または延長であることを示す実装および実験的エビデンスを提供する。
モデル検査コンペティションによる大規模な(ランダムな)ベンチマーク実験のパフォーマンスは、半決定手順であるにもかかわらず、この手法は依然として技術検証ツールの状態を改善することができることを示している。
関連論文リスト
- Unlikelihood Tuning on Negative Samples Amazingly Improves Zero-Shot
Translation [79.96416609433724]
Zero-shot Translation (ZST)は、トレーニングデータにおいて、目に見えない言語ペア間の翻訳を目的としている。
推論中にゼロショット言語マッピングをガイドする一般的な方法は、ソースとターゲット言語IDを意図的に挿入することである。
近年の研究では、言語IDが時折ZSTタスクのナビゲートに失敗し、ターゲット外問題に悩まされることが示されている。
論文 参考訳(メタデータ) (2023-09-28T17:02:36Z) - Analyzing and Reducing the Performance Gap in Cross-Lingual Transfer
with Fine-tuning Slow and Fast [50.19681990847589]
既存の研究では、1つの(ソース)言語で微調整された多言語事前学習言語モデルが、非ソース言語の下流タスクでもうまく機能していることが示されている。
本稿では、微調整プロセスを分析し、パフォーマンスギャップがいつ変化するかを分析し、ネットワークの重みが全体のパフォーマンスに最も影響するかを特定する。
論文 参考訳(メタデータ) (2023-05-19T06:04:21Z) - Estimating the Adversarial Robustness of Attributions in Text with
Transformers [44.745873282080346]
リプシッツ連続性に基づくテキスト分類における帰属ロバスト性(AR)の新たな定義を確立する。
そこで我々は,テキスト分類における属性の厳密な推定を行う強力な敵であるTransformerExplanationAttack (TEA)を提案する。
論文 参考訳(メタデータ) (2022-12-18T20:18:59Z) - DEMETR: Diagnosing Evaluation Metrics for Translation [21.25704103403547]
我々は、英語31K例の診断データセットであるDEMETRをリリースする。
学習指標はDEMETRの文字列ベースの指標よりもかなり優れていることがわかった。
論文 参考訳(メタデータ) (2022-10-25T03:25:44Z) - Data Augmentation to Address Out-of-Vocabulary Problem in Low-Resource
Sinhala-English Neural Machine Translation [1.2891210250935146]
Out-of-Vocabulary(OOV)はニューラルマシン翻訳(NMT)の問題である
両種類のOOVを考慮した単語とフレーズの置換に基づくデータ拡張(DA)手法を提案する。
単語の構文的および意味的特性は、合成文の流布を保証するために考慮する。
論文 参考訳(メタデータ) (2022-05-18T04:52:43Z) - Block-Sparse Adversarial Attack to Fool Transformer-Based Text
Classifiers [49.50163349643615]
本稿では,変圧器を用いたテキスト分類器に対して,勾配に基づく逆攻撃を提案する。
実験結果から, 文の意味を抑えながら, GPT-2の精度を5%以下に抑えることができた。
論文 参考訳(メタデータ) (2022-03-11T14:37:41Z) - Autoregressive Belief Propagation for Decoding Block Codes [113.38181979662288]
誤り訂正符号の復号化にグラフニューラルネットワークを用いた最近の手法を再検討する。
本手法は,他手法がゼロワードでのみ学習できる対称性条件に反する。
1つの単語でトレーニングする余地がなく、関連するサンプル空間のごく一部でトレーニングできないにもかかわらず、効果的なトレーニングを実演する。
論文 参考訳(メタデータ) (2021-01-23T17:14:55Z) - Boosting Continuous Sign Language Recognition via Cross Modality
Augmentation [135.30357113518127]
連続手話認識は不整合のビデオテキストペアを扱う。
クロスモーダル拡張を用いた新しいアーキテクチャを提案する。
提案するフレームワークは、既存のCTCベースの連続SLRアーキテクチャに容易に拡張できる。
論文 参考訳(メタデータ) (2020-10-11T15:07:50Z) - Contextualized Perturbation for Textual Adversarial Attack [56.370304308573274]
逆例は自然言語処理(NLP)モデルの脆弱性を明らかにする。
本稿では,フロートおよび文法的出力を生成するContextualized AdversaRial Example生成モデルであるCLAREを提案する。
論文 参考訳(メタデータ) (2020-09-16T06:53:15Z) - Improved Natural Language Generation via Loss Truncation [29.676561106319173]
識別性は、無効な参照を扱うための原則的で堅牢な代替手段であることを示す。
学習中に高損失例を適応的に除去する損失トランケーションを提案する。
これは、ログの損失やノイズ下での識別性を厳格に制限するのと同じくらい簡単に最適化できることを示している。
論文 参考訳(メタデータ) (2020-04-30T05:31:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。