Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
复制标题
具有最大不动点的 Hennessy-Milner 逻辑作为完整的行为规范理论
DOI：
10.1007/978-3-642-40184-8_7
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Axel Legay
中科院分区：
文献类型：
--
作者：
Nikola Benes;Benoît Delahaye;U. Fahrenberg;Jan Křetínský;Axel Legay
有两种根本不同的方法来指定和验证系统的属性。逻辑方法利用以时间或模态逻辑公式给出的规范，并依赖于有效的模型检查算法；行为方法利用各种等价或细化检查方法，前提是规范以与实现相同的形式给出。
在本文中，我们提供了具有最大不动点的 Hennessy-Milner 逻辑的逻辑形式主义和析取模态转换系统的行为形式主义之间的转换。我们还为上述等效形式引入了一种新的商运算，它与结构组合相关，并允许从部分实现中合成缺失的规范。这是早期论文中定义的确定性模态转换系统商的实质性概括。
There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations.
In this paper we provide translations between the logical formalism of Hennessy-Milner logic with greatest fixed points and the behavioural formalism of disjunctive modal transition systems. We also introduce a new operation of quotient for the above equivalent formalisms, which is adjoint to structural composition and allows synthesis of missing specifications from partial implementations. This is a substantial generalisation of the quotient for deterministic modal transition systems defined in earlier papers.