Determinizing monitors for HML with recursion.

Journal of Logical and Algebraic Methods in Programming(2020)

引用 16|浏览39
暂无评分
摘要
We examine the determinization of monitors for HML with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (or as their labeled transition systems), then they can be exponentially more succinct than their CCS process form.
更多
查看译文
关键词
Monitorability,Runtime verification,Hennessy-Milner logic,Determinization,Complexity bounds
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要