AI 中文总结
研究引入高阶模态不动点逻辑的余代数扩展，包含HFL及其概率扩展，证明非确定性有限自动机空集问题和概率自动机值为1问题可归结为该余代数形式的模型检查问题。
AI 中文摘要
我们引入了高阶模态不动点逻辑（HFL）的余代数扩展，它包含了HFL及其概率扩展。我们证明了非确定性有限自动机的空集问题以及概率自动机的值为1的问题都可归结为这种HFL余代数形式的模型检查问题。
英文摘要
We introduce a coalgebraic extension of the higher-order modal fixed-point logic (HFL) which subsumes both HFL and its probabilistic extension. We show that the emptiness problem for non-deterministic finite automata as well as the value-1 problem for probabilistic automata reduce to model-checking problems for this coalgebraic formulation of HFL.
Comments17 pages
