带递归的 HML 监控器的确定化
计算机科学中的逻辑
2016-12-01 v1 形式语言与自动机理论
摘要
我们研究带递归的 HML 监控器的确定化。我们证明每个监控器都等价于一个确定性监控器,其规模相对于原监控器至多为双指数级。当监控器被描述为类 CCS 进程时,此双指数界是最优的。当(确定性)监控器被描述为有限自动机(作为其 LTS)时,它们可以比其 CCS 进程形式指数级更简洁。
引用
@article{arxiv.1611.10212,
title = {Determinizing Monitors for HML with Recursion},
author = {Luca Aceto and Antonis Achilleos and Adrian Francalanza and Anna Ingólfsdóttir and Sævar Örn Kjartansson},
journal= {arXiv preprint arXiv:1611.10212},
year = {2016}
}