論文の概要: On Synthesis of Timed Regular Expressions
- arxiv url: http://arxiv.org/abs/2509.06262v1
- Date: Mon, 08 Sep 2025 00:59:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-09 14:07:03.926484
- Title: On Synthesis of Timed Regular Expressions
- Title(参考訳): 時間正規表現の合成について
- Authors: Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang, Zhenya Zhang,
- Abstract要約: タイムレギュラー表現は、サイバー物理システムのリアルタイム動作を特定するフォーマリズムとして機能する。
本稿では, 時間的正規表現の合成について考察し, 時間的正規表現の生成とシステム挙動の整合性に着目した。
- 参考スコア(独自算出の注目度): 8.729947740812237
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Timed regular expressions serve as a formalism for specifying real-time behaviors of Cyber-Physical Systems. In this paper, we consider the synthesis of timed regular expressions, focusing on generating a timed regular expression consistent with a given set of system behaviors including positive and negative examples, i.e., accepting all positive examples and rejecting all negative examples. We first prove the decidability of the synthesis problem through an exploration of simple timed regular expressions. Subsequently, we propose our method of generating a consistent timed regular expression with minimal length, which unfolds in two steps. The first step is to enumerate and prune candidate parametric timed regular expressions. In the second step, we encode the requirement that a candidate generated by the first step is consistent with the given set into a Satisfiability Modulo Theories (SMT) formula, which is consequently solved to determine a solution to parametric time constraints. Finally, we evaluate our approach on benchmarks, including randomly generated behaviors from target timed models and a case study.
- Abstract(参考訳): タイムレギュラー表現は、サイバー物理システムのリアルタイム動作を特定するフォーマリズムとして機能する。
本稿では,時間的正規表現の合成について考察し,正および負の例を含むシステム動作の所定のセットに整合した時間的正規表現の生成に着目し,すべての正の例を受け入れ,すべての負の例を拒絶する。
まず、簡単な時間的正規表現の探索を通して合成問題の決定可能性を証明する。
そこで本研究では,最小長の連続時間正規表現を2段階に展開する手法を提案する。
最初のステップは、パラメトリックな時間的正規表現を列挙し、プルーーンすることです。
第2のステップでは、第1のステップで生成された候補が与えられた集合と一致しているという要件をSMT(Satifiability Modulo Theories)公式にエンコードし、パラメトリック時間制約の解を決定する。
最後に、対象の時間モデルからランダムに生成された振る舞いやケーススタディを含む、ベンチマークに対するアプローチを評価した。
関連論文リスト
- Real-time Regular Expression Matching [65.268245109828]
本稿では,有限状態オートマトン,正規表現マッチング,パターン認識,指数的爆破問題について述べる。
本稿では,正規言語の複雑なクラスに対する指数的爆破問題に対する理論的およびハードウェア的解法を提案する。
論文 参考訳(メタデータ) (2023-08-20T09:25:40Z) - Euclidean time method in Generalized Eigenvalue Equation [0.0]
一般化固有値方程式 $A ketphi_n を解くための変分量子固有解器のユークリッド時間法を開発した。
論文 参考訳(メタデータ) (2023-07-27T06:20:12Z) - Compositional Generalization without Trees using Multiset Tagging and
Latent Permutations [121.37328648951993]
まず、各入力トークンに複数の出力トークンをタグ付けします。
次に、新しいパラメータ化法と置換予測法を用いて、トークンを出力シーケンスに配置する。
我々のモデルは、事前訓練されたセq2seqモデルと、現実的なセマンティック解析タスクに関する先行研究より優れている。
論文 参考訳(メタデータ) (2023-05-26T14:09:35Z) - Near-Optimal Non-Parametric Sequential Tests and Confidence Sequences
with Possibly Dependent Observations [44.71254888821376]
我々は、一般的な非データ生成プロセスの下で、最初のタイプIエラーと予測リジェクション時間保証を提供する。
本研究では, 平均処理効果など, 方程式を推定することによって定義されるパラメータの推測に, 結果を適用する方法を示す。
論文 参考訳(メタデータ) (2022-12-29T18:37:08Z) - Time Dependent Hamiltonian Simulation Using Discrete Clock Constructions [42.3779227963298]
時間依存力学を時間依存システムとして符号化するためのフレームワークを提供する。
まず、拡張クロックシステム上で量子化を行う時間依存シミュレーションアルゴリズムを作成する。
第2に、時間順序指数に対する多積公式の自然な一般化を定義する。
論文 参考訳(メタデータ) (2022-03-21T21:29:22Z) - Proving Equivalence Between Complex Expressions Using Graph-to-Sequence
Neural Models [0.0]
プログラム同値性のためのグラフ・ツー・シーケンスニューラルネットワークシステムを開発した。
我々は、リッチな多型線形代数表現言語を用いて、我々のシステムを広範囲に評価する。
我々の機械学習システムは、全ての真正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の
論文 参考訳(メタデータ) (2021-06-01T20:45:42Z) - FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions [5.21480688623047]
デジタルフォームバリデーションのための正規表現シンセサイザーであるFORESTについて紹介する。
forestryは入力値の所望のパターンにマッチする正規表現を生成する。
また、与えられた正規表現のキャプチャ条件を合成する新しいSMTエンコーディングも提案する。
論文 参考訳(メタデータ) (2020-12-28T14:06:01Z) - Adaptive Sequential SAA for Solving Two-stage Stochastic Linear Programs [1.6181085766811525]
大規模2段階線形プログラムを解くための適応的逐次SAA(sample average approximation)アルゴリズムを提案する。
提案アルゴリズムは,品質の確率論的保証が与えられた解を返すために,有限時間で停止することができる。
論文 参考訳(メタデータ) (2020-12-07T14:58:16Z) - Orbital MCMC [82.54438698903775]
任意の微分同相写像から周期軌道を構築するための2つの実用的なアルゴリズムを提案する。
また,両カーネルの実用的メリットを実証した実証的研究を行った。
論文 参考訳(メタデータ) (2020-10-15T22:25:52Z) - Pseudo-Convolutional Policy Gradient for Sequence-to-Sequence
Lip-Reading [96.48553941812366]
唇読解は唇運動系列から音声内容を推測することを目的としている。
seq2seqモデルの伝統的な学習プロセスには2つの問題がある。
本稿では,これら2つの問題に対処するために,PCPGに基づく新しい手法を提案する。
論文 参考訳(メタデータ) (2020-03-09T09:12:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。