公理化无递归的常规监视器
Axiomatizing recursion-free, regular monitors
摘要：
线程是运行时验证领域的一个关键工具，它们通过分析进程生成的执行跟踪来验证系统属性。Aceto等人在一系列论文中对运行时监控进行了研究。$~$使用Milner的CCS的常规片段的变体指定了监控器，并研究了监控器上两个基于跟踪的等价概念，即判定和$ω$ -判定等价。这篇文章致力于研究监察员模这两个等价概念的等式逻辑。它提出了完整的等式公理化的裁决和$ω$裁决等价的封闭和开放的条件下，递归自由监测。当动作集是有限的且至少包含两个动作时，开监控器上的判决等价没有有限的等式公理化。
英文摘要：
Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al.$~$has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and $ω$-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and $ω$-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
