2012
Modal Transition Systems with Weight Intervals
JUHL, Line; Kim G. LARSEN a Jiří SRBAZákladní údaje
Originální název
Modal Transition Systems with Weight Intervals
Název česky
Modalni prechodove systemy s ohodnocenymi intervaly
Autoři
JUHL, Line; Kim G. LARSEN a Jiří SRBA
Vydání
Journal of Logic and Algebraic Programming, Elsevier, 2012, 1567-8326
Další údaje
Jazyk
angličtina
Typ výsledku
Článek v odborném periodiku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Nizozemské království
Utajení
není předmětem státního či obchodního tajemství
Impakt faktor
Impact factor: 0.529
Označené pro přenos do RIV
Ne
Organizační jednotka
Fakulta informatiky
UT WoS
Klíčová slova česky
modalni prechodove systemy; logika
Klíčová slova anglicky
modal transition systems; logic
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 28. 4. 2015 00:23, RNDr. Pavel Šmerk, Ph.D.
V originále
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.
Česky
Navrhujeme vážený modální transformace systému, rozšíření dobře studoval specifikace formalismu modální transformace systémů, která umožňuje vyjádřit povinných a nepovinných chování zamýšlené implementace. V naší rozšíření zdobíme každý přechod s hmotností interval, který označuje řadu konkrétních hodnot hmotnosti k dispozici možnost implementace. Tímto způsobem je možné omezené zdroje je modelován pomocí modální přístup. Zaměřujeme se na dva problémy. Nejprve sledujeme otázku existence / najít největší společný pro celou řadu vylepšení konečných deterministických specifikací a ukážeme PSPACE-úplnost problému. Výstavbou nejobecnější společné zjemnění, počítáme s postupným a opakující se budování společné implementace. Za druhé, studujeme logickou charakteristiku formalismu a ukázat, že vzorec v přírodním hmotnosti rozšíření logiky CTL jsou splněny určité modální specifikace tehdy a jen tehdy, pokud je splněna ve všech jeho zdokonalení. Hmotnost rozšíření obecně stačí k vyjádření různých druhů vlastností, které chceme, aby naše váhy uspokojit.
Návaznosti
| MSM0021622419, záměr |
|