关于无限字上的 MITL 与交替时间自动机
计算机科学中的逻辑
2014-06-18 v1 逻辑
摘要
单时钟交替时间自动机 (OCATA) 被引入作为（单时钟）时间自动机的自然扩展，以表达 MTL 的语义。在本文中，我们考虑将 OCATA 应用于 MITL（MTL 的一个语法片段）在无限字解释下的模型检测与可满足性问题。我们的方法基于区间语义（最近在 [BEG13] 中针对有限字情况引入），并将其扩展至无限字。基于此语义，我们提出了用于 MITL 模型检测和可满足性的基于区域 (region-based) 和基于区 (zone-based) 的算法。我们报告了实现这些算法的原型工具的性能表现。
引用
@article{arxiv.1406.4395,
title = {On MITL and alternating timed automata over infinite words},
author = {Thomas Brihaye and Morgane Estiévenart and Gilles Geeraerts},
journal= {arXiv preprint arXiv:1406.4395},
year = {2014}
}