带未来折扣的线性时序逻辑的近最优调度
计算机科学中的逻辑
2015-11-10 v4
摘要
我们研究了带未来折扣的线性时序逻辑 (LTL) 的最优调度器搜索问题。该逻辑由 Almagor、Boker 和 Kupferman 引入，是 LTL 的一种定量变体，其中遥远未来的事件对真值（即单位区间 [0, 1] 内的实数）仅具有折扣贡献。我们研究的具体问题自然出现于例如搜索能尽快从内部错误状态恢复的调度器场景中，其描述如下：给定一个 Kripke 框架、一个公式以及一个称为容差的 [0, 1] 区间内的数值，寻找一条相对于该公式在 prescribed 容差范围内最优的 Kripke 框架路径（真正的最优路径可能不存在）。我们提出了一种针对该问题的算法；即使在包含命题质量算子的扩展设定下，该算法依然有效，而在该设定中（阈值）模型检测已知是不可判定的。
引用
@article{arxiv.1410.4950,
title = {Near-Optimal Scheduling for LTL with Future Discounting},
author = {Shota Nakagawa and Ichiro Hasuo},
journal= {arXiv preprint arXiv:1410.4950},
year = {2015}
}