Modal transition systems with weight intervals

详细信息	查看全文 | 推荐本文 |

• 作者：Line Juhl ; ^{linej@cs.aau.dk} ; Kim G. Larsen ^{kgl@cs.aau.dk} ; Ji艡谋´ ; Srba¹ ; ^{srba@cs.aau.dk}
• 关键词：Modal transition systems ; Weighted transition systems ; Deterministic specifications ; Refinement ; Action-based CTL ; Model checking
• 刊名：Journal of Logic and Algebraic Programming
• 出版年：2012
• 期刊代码：73_15678326
• 类别：cp
• 出版时间：May, 2012
• 卷：81
• 期：4
• 页码：408-421
• 文件大小：509 K

摘要

We propose weighted modal transition systems, an extension to the well-studied specification formalism of modal transition systems that allows to express both required and optional behaviours of their intended implementations. In our extension we decorate each transition with a weight interval that indicates the range of concrete weight values available to the potential implementations. In this way resource constraints can be modelled using the modal approach. We focus on two problems. First, we study the question of existence/finding the largest common refinement for a number of finite deterministic specifications and we show PSPACE-completeness of this problem. By constructing the most general common refinement, we allow for a stepwise and iterative construction of a common implementation. Second, we study a logical characterisation of the formalism and show that a formula in a natural weight extension of the logic CTL is satisfied by a given modal specification if and only if it is satisfied by all its refinements. The weight extension is general enough to express different sorts of properties that we want our weights to satisfy.