Publication details

Modal Transition Systems with Weight Intervals

Authors

JUHL Line LARSEN Kim G. SRBA Jiří

Year of publication 2012
Type Article in Periodical
Magazine / Source Journal of Logic and Algebraic Programming
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1016/j.jlap.2012.03.008
Field Informatics
Keywords modal transition systems; logic
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info