Decision Problems for Partial Specifications : Empirical and Worst-Case Complexities
Decision Problems for Partial Specifications : Empirical and Worst-Case Complexities
复制标题
部分规范的决策问题：经验和最坏情况的复杂性
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Adam Antonik
中科院分区：
文献类型：
--
作者：
Adam Antonik
部分规范允许创建系统的近似模型，例如Kripke结构或标记的过渡系统。使用这些模型可能的抽象，可以避免状态空间爆炸问题，同时仍然保留可以对其进行属性检查的结构。单个部分规范抽象了一组系统，无论是Kripke、标记转换系统，还是同时具有原子命题和命名转换的系统。本文部分地讨论了在部分规范上对模态μ微积分的句子进行有效求值所引起的问题。部分规范还允许通过多个部分规范对单个系统进行建模，这些部分规范抽象出系统的不同部分。另外，许多部分规范可能表示系统上的不同需求。本文还讨论了一组部分规范是否一致的问题，也就是说，是否存在由该集合的每个成员抽象的单个系统。在许多部分规范的一致性问题上，也考虑了标称的影响，即在系统中只对一个状态为真的特殊原子命题。本文还讨论了部分规范抽象的系统是否都被第二部分规范抽象的问题，即包含问题。本文论证了常用的“规范模式”——模态μ微积分中指定的有用性质——如何在部分规范上有效地求值，并给出了与部分规范集有关的问题的上、下复杂度界。
Partial specifications allow approximate models of systems such as Kripke structures, or labeled transition systems to be created. Using the abstraction possible with these models, an avoidance of the state-space explosion problem is possible, whilst still retaining a structure that can have properties checked over it. A single partial specification abstracts a set of systems, whether Kripke, labeled transition systems, or systems with both atomic propositions and named transitions. This thesis deals in part with problems arising from a desire to efficiently evaluate sentences of the modal μ-calculus over a partial specification. Partial specifications also allow a single system to be modeled by a number of partial specifications, which abstract away different parts of the system. Alternatively, a number of partial specifications may represent different requirements on a system. The thesis also addresses the question of whether a set of partial specifications is consistent, that is to say, whether a single system exists that is abstracted by each member of the set. The effect of nominals, special atomic propositions true on only one state in a system, is also considered on the problem of the consistency of many partial specifications. The thesis also addresses the question of whether the systems a partial specification abstracts are all abstracted by a second partial specification, the problem of inclusion. The thesis demonstrates how commonly used “specification patterns” – useful properties specified in the modal μ-calculus, can be efficiently evaluated over partial specifications, and gives upper and lower complexity bounds on the problems related to sets of partial specifications.
论语义自我最小化的复杂性
影响因子：
--
作者：
Antonik A
通讯作者：
Antonik A