关于 TPTL 和 MTL 在$\omega$-数据字上的表达能力
计算机科学中的逻辑
2014-05-23 v2
摘要
度量时序逻辑（Metric Temporal Logic, MTL）和定时命题时序逻辑（Timed Propositional Temporal Logic, TPTL）是线性时序逻辑的重要扩展，用于指定数据语言的性质。在本文中，我们考虑自然数上非单调数据字的数据语言类。我们证明，在此设定下，TPTL 的表达能力严格强于 MTL。为此，我们为 MTL 引入了 Ehrenfeucht-Fraisse (EF) 博弈。利用 MTL 的 EF 博弈，我们还证明了 MTL 可定义性判定问题（“给定一个 TPTL 公式，该公式定义的语言是否可用 MTL 定义？”）是不可判定的。我们还定义了 TPTL 的 EF 博弈，并展示了各种句法限制对 MTL 和 TPTL 表达能力的影响。
引用
@article{arxiv.1311.6250,
title = {On the Expressiveness of TPTL and MTL over \omega-Data Words},
author = {Claudia Carapelle and Shiguang Feng and Oliver Fernández Gil and Karin Quaas},
journal= {arXiv preprint arXiv:1311.6250},
year = {2014}
}
备注
In Proceedings AFL 2014, arXiv:1405.5272