BriefGPT - AI 论文速递
·
多变量一侧间隔 TPTL 的可满足性检查是 PSPACE - 完全的
💡
原文中文，约700字，阅读约需2分钟。
📝
内容提要
本文研究了Timed Propositional Temporal Logic (TPTL)的{0,∞}分片的可决定性，并证明了TPTL^{0,∞}的可满足性检查为PSPACE-complete。此外，1-TPTL^{0,∞}比Metric Interval Temporal Logic (MITL)更具表达能力，后者的可满足性检查是EXPSPACE complete。因此，TPTL^{0,∞}是第一个多变量TPTL分片，其可满足性检查在没有对时态词施加任何限制的情况下是可决定的。通过将其规约到Unilateral Very Weak Alternating Timed Automata (VWATA^{0,∞})的空泛性检查问题，我们证明了PSPACE的成员关系。
🎯
关键要点
- 研究了Timed Propositional Temporal Logic (TPTL)的{0,∞}分片的可决定性。
- 证明了TPTL^{0,∞}的可满足性检查为PSPACE-complete。
- 1-TPTL^{0,∞}比Metric Interval Temporal Logic (MITL)更具表达能力。
- MITL的可满足性检查是EXPSPACE complete。
- TPTL^{0,∞}是第一个多变量TPTL分片，其可满足性检查在没有对时态词施加任何限制的情况下是可决定的。
- 通过将其规约到Unilateral Very Weak Alternating Timed Automata (VWATA^{0,∞})的空泛性检查问题，证明了PSPACE的成员关系。
- 构造了与给定VWATA^{0,∞}的大小多项式相关的非确定性时态自动机的模拟等价关系。
➡️
