加权定时自动机与加权相对距离逻辑的Nivat定理
形式语言与自动机理论
2015-06-22 v1
摘要
加权定时自动机(WTA)对实时系统的定量方面进行建模，例如内存、功耗或财务资源的持续消耗。它们接收定量定时语言，其中每个定时词被映射到一个值，例如实数。本文证明了WTA的一个Nivat定理，该定理指出，可识别的定量定时语言恰好是那些借助若干简单操作从可识别的布尔定时语言获得的语言。我们还引入了由Wilke提出的相对距离逻辑的加权扩展，并证明了我们的加权相对距离逻辑与WTA具有相同的表达能力。该结果的证明可由我们的Nivat定理和Wilke的相对距离逻辑定理推导得出。由于我们的Nivat定理证明是构造性的，从逻辑到自动机及反之亦然的翻译过程也是构造性的。这导致了加权相对距离逻辑的可判定性结果。
引用
@article{arxiv.1506.06038,
title = {A Nivat Theorem for Weighted Timed Automata and Weighted Relative Distance Logic},
author = {Manfred Droste and Vitaly Perevoshchikov},
journal= {arXiv preprint arXiv:1506.06038},
year = {2015}
}
备注
The final version appeared in the Proceedings of the 41st International Colloquium on Automata, Languages, and Programming (ICALP 2014)