论文标题
模型检查和模型综合部分模型：基于逻辑的视角
Model checking and model synthesisfrom partial models: a logic-based perspective
论文作者
论文摘要
我考虑以下一般方案：某些“真实”系统的抽象模型M仅部分呈现或部分呈现给我们，我们必须确保实际系统满足以某种逻辑语言形式化的给定规范。这种情况至少具有两个本质上不同的解释，导致两个基本不同的，正式的逻辑和算法问题：“模型综合部分模型”，其中某些“可接受”将M扩展到完整模型必须满足规范，并且“对部分模型的模型检查”，其中所有“可允许”的模型都必须满足完整模型的扩展。这些问题自然会扩大可满足性，有效性和模型检查的经典逻辑决策问题。 在这里，我在经典，模态和时间逻辑的背景下简要讨论这两个问题。我进行了一些观察，陈述了一些空旷的问题，并概述了一般的Tableaux式程序，该过程解决了从有限的部分模型中解决了不受限制的模型合成问题，用于几种众所周知的模态和时间逻辑，包括。 K，LTL，CTL，ATL。
I consider the following generic scenario: an abstract model M of some 'real' system is only partially presented, or partially known to us, and we have to ensure that the actual system satisfies a given specification, formalised in some logical language. This scenario has at least two essentially different interpretations, leading to two, essentially different, formal logical and algorithmic problems: "Model Synthesis from Partial Models", where some 'admissible' extension of M to a full model must satisfy the specification, and "Model Checking of Partial Models", where all 'admissible' extensions of M to a full model must satisfy the specification. These problems naturally extend the classical logical decision problems of Satisfiability, Validity, and Model Checking. Here I briefly discuss both problems in the contexts of classical, modal and temporal logics. I make some observations, state some open questions, and outline a general tableaux-style procedure that solves the problem of unconstrained model synthesis from finite partial models for several well-known modal and temporal logics, incl. K, LTL, CTL, ATL.
