Logical Characterisation of Hybrid Conformance
Logical Characterisation of Hybrid Conformance
复制标题
混合一致性的逻辑表征
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
M. Mousavi
中科院分区：
文献类型：
--
作者：
Maciej Gazda;M. Mousavi
行为等价关系的逻辑表征精确地指定了由该关系保留和反映的公式集。这种特性已经被广泛研究的精确语义离散模型，如互模拟标记的过渡系统和Kripke结构，但在很小的程度上近似关系，特别是在混合动力系统的上下文中。我们提出了什么是我们所知的第一个表征结果的近似概念的混合细化和混合一致性涉及公差阈值的时间和价值。由于在这种情况下，一致性的概念是近似的，任何表征都必然涉及放松的概念，表示规范公式应该如何放松，以保持实现。我们还表明，现有的松弛计划度量时态逻辑用于保存结果，在这种设置是不够紧，既不混合一致性，也不细化提供一个表征。表征的结果，而有趣的是在其本身的权利，铺平了道路，更多的应用研究，因为我们的概念的混合一致性的基础上正式的基于模型的技术验证的网络物理系统。
Logical characterisation of a behavioural equivalence relation precisely specifies the set of formulae that are preserved and reflected by the relation. Such characterisations have been studied extensively for exact semantics on discrete models such as bisimulations for labelled transition systems and Kripke structures, but to a much lesser extent for approximate relations, in particular in the context of hybrid systems. We present what is to our knowledge the first characterisation result for approximate notions of hybrid refinement and hybrid conformance involving tolerance thresholds in both time and value. Since the notion of conformance in this setting is approximate, any characterisation will unavoidably involve a notion of relaxation, denoting how the specification formulae should be relaxed in order to hold for the implementation. We also show that an existing relaxation scheme on Metric Temporal Logic used for preservation results in this setting is not tight enough for providing a characterisation of neither hybrid conformance nor refinement. The characterisation result, while interesting in its own right, paves the way to more applied research, as our notion of hybrid conformance underlies a formal model-based technique for the verification of cyber-physical systems.