論文の概要: Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals
Is PSPACE-Complete
- arxiv url: http://arxiv.org/abs/2309.00386v1
- Date: Fri, 1 Sep 2023 10:49:19 GMT
- ステータス: 処理完了
- システム内更新日: 2023-09-04 13:41:57.906611
- Title: Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals
Is PSPACE-Complete
- Title（参考訳）: PSPACE-Completeによる多変数TPTLの満足度検証
- Authors: Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar,
Paritosh K. Pandya
- Abstract要約: 時間命題時間論理(TPTL)の0,infty$フラグメントの決定可能性について検討する。
TPTL$0,infty$はPSPACE完全であることを示す。
- 参考スコア（独自算出の注目度）: 6.4810099964297665
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We investigate the decidability of the ${0,\infty}$ fragment of Timed
Propositional Temporal Logic (TPTL). We show that the satisfiability checking
of TPTL$^{0,\infty}$ is PSPACE-complete. Moreover, even its 1-variable fragment
(1-TPTL$^{0,\infty}$) is strictly more expressive than Metric Interval Temporal
Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we
have a strictly more expressive logic with computationally easier
satisfiability checking. To the best of our knowledge, TPTL$^{0,\infty}$ is the
first multi-variable fragment of TPTL for which satisfiability checking is
decidable without imposing any bounds/restrictions on the timed words (e.g.
bounded variability, bounded time, etc.). The membership in PSPACE is obtained
by a reduction to the emptiness checking problem for a new "non-punctual"
subclass of Alternating Timed Automata with multiple clocks called Unilateral
Very Weak Alternating Timed Automata (VWATA$^{0,\infty}$) which we prove to be
in PSPACE. We show this by constructing a simulation equivalent
non-deterministic timed automata whose number of clocks is polynomial in the
size of the given VWATA$^{0,\infty}$.
- Abstract（参考訳）: 時間命題時間論理(TPTL)の${0,\infty}$フラグメントの決定可能性について検討する。
TPTL$^{0,\infty}$ の満足度チェックは PSPACE 完全であることを示す。
さらに、その 1-変数の断片 (1-TPTL$^{0,\infty}$) でさえ、満足度チェックが EXPSPACE 完全であるMetric Interval Temporal Logic (MITL) よりも厳密に表現できる。
したがって、計算が容易で満足度チェックが可能な、厳密な表現力のある論理が存在する。
我々の知る限り、TPTL$^{0,\infty}$ は TPTL の最初の多変量フラグメントであり、満足度チェックは時間付き単語(例えば、有界変数、有界時間など)に境界や制限を課すことなく決定可能である。
PSPACE のメンバシップは、PSPACE に含まれることを証明した、片側超弱交換時間オートマタ (VWATA$^{0,\infty}$) と呼ばれる複数のクロックを持つ交代時間オートマタの新しい「非変動」サブクラスに対する空度チェック問題に還元することで得られる。
クロック数が与えられた VWATA$^{0,\infty}$ の大きさの多項式である非決定論的時間付きオートマトンをシミュレーションで構築することにより、これを示す。
関連論文リスト
- Anytime Acceleration of Gradient Descent [92.02082223856479]
我々は,任意の停止時間に対して,勾配降下が$O(T-1.03)$の収束保証を達成するための段階的スケジュールを提案する。
我々はこの理論を拡張して、滑らかで強い凸最適化のために$exp(-Omega(T/kappa0.97)$の収束を保証する。
論文 参考訳（メタデータ） (2024-11-26T18:29:44Z) - LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces [44.35335751462176]
オートマチックf+/PPLTL+のためのDFAベースの合成技術について述べる。
PPLTL+の表現力は2EXPTIME完全ではなくEXPTIME完全であることを示す。
論文 参考訳（メタデータ） (2024-11-14T11:17:06Z) - Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。
有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
論文 参考訳（メタデータ） (2023-07-31T17:02:23Z) - Run Time Bounds for Integer-Valued OneMax Functions [0.9012198585960443]
探索空間 $mathbbZn$ を多値決定変数 $0,ldots,r-1n$ の観点から考える。
ステップサイズ適応のRSSが$Theta(n cdot log(|a|_1))$の最適化時間を達成することを示す。
本稿では,これらのアルゴリズムを離散探索空間に対するCMA-ESの変種と比較し,実験的な解析を行った。
論文 参考訳（メタデータ） (2023-07-21T18:49:06Z) - Efficient Quantum State Synthesis with One Query [0.0]
本稿では,古典的オラクルへの単一クエリ(重ね合わせ)を実現する時間類似量子アルゴリズムを提案する。
我々は、すべての$n$-qubit状態が、適切な有限ゲート集合上の$On/n)$-size回路によって0.01エラー内に構築可能であることを証明した。
論文 参考訳（メタデータ） (2023-06-02T17:49:35Z) - Non-stationary Online Convex Optimization with Arbitrary Delays [50.46856739179311]
本稿では,非定常環境における遅延オンライン凸最適化(OCO)について検討する。
まず, 遅延勾配の勾配降下ステップを, 到着順に応じて行う単純なアルゴリズム, DOGDを提案する。
DOGDが達成した動的後悔境界を$O(sqrtbardT(P_T+1))$に削減する改良アルゴリズムを開発した。
論文 参考訳（メタデータ） (2023-05-20T07:54:07Z) - Optimal Query Complexities for Dynamic Trace Estimation [59.032228008383484]
我々は,行列がゆっくりと変化している動的環境において,正確なトレース推定に必要な行列ベクトルクエリ数を最小化する問題を考える。
我々は、$delta$失敗確率で$epsilon$エラーまで、すべての$m$トレースを同時に推定する新しいバイナリツリー要約手順を提供する。
我々の下界(1)は、静的な設定においてもフロベニウスノルム誤差を持つ行列ベクトル積モデルにおけるハッチンソン推定子の第一の厳密な境界を与え、(2)動的トレース推定のための最初の無条件下界を与える。
論文 参考訳（メタデータ） (2022-09-30T04:15:44Z) - The Parameterized Complexity of Quantum Verification [7.7155343772895275]
量子回路の整合性の問題に対して,非クリフォードゲート数で指数関数的にスケーリングすることで問題を解くアルゴリズムが存在することを示す。
我々は、サーキット適合性のインスタンスの$T$-countと$W$-stateの$$$-countに新しい下位境界を導出する。
論文 参考訳（メタデータ） (2022-02-16T14:53:42Z) - An Optimal Separation of Randomized and Quantum Query Complexity [67.19751155411075]
すべての決定木に対して、与えられた順序 $ellsqrtbinomdell (1+log n)ell-1,$ sum to at least $cellsqrtbinomdell (1+log n)ell-1,$ where $n$ is the number of variables, $d$ is the tree depth, $c>0$ is a absolute constant。
論文 参考訳（メタデータ） (2020-08-24T06:50:57Z) - A polynomial time and space heuristic algorithm for T-count [2.28438857884398]
この研究は、最先端のフォールトトレラントな量子エラー訂正符号を使用する場合の量子アルゴリズム実装の物理的コストの低減に重点を置いている。
普遍ゲート集合であるクリフォード+Tゲート集合からなる量子回路によって正確に実装できるユニタリ群を考える。
論文 参考訳（メタデータ） (2020-06-22T17:21:41Z) - Fixed-Support Wasserstein Barycenters: Computational Hardness and Fast
Algorithm [100.11971836788437]
固定支持ワッサーシュタインバリセンタ問題(FS-WBP)について検討する。
我々は,有望な反復的ブレグマン射影 (IBP) アルゴリズムであるtextscFastIBP の,証明可能な高速なテキスト決定論的変種を開発する。
論文 参考訳（メタデータ） (2020-02-12T03:40:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。