Refinement checking on parametric modal transition systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F15%3A00080734" target="_blank" >RIV/00216224:14330/15:00080734 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/s00236-015-0215-4" target="_blank" >http://dx.doi.org/10.1007/s00236-015-0215-4</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s00236-015-0215-4" target="_blank" >10.1007/s00236-015-0215-4</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Refinement checking on parametric modal transition systems

Popis výsledku v původním jazyce

Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many ofthe limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking.

Název v anglickém jazyce

Refinement checking on parametric modal transition systems

Popis výsledku anglicky

Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many ofthe limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Acta Informatica

ISSN

0001-5903

e-ISSN

—

Svazek periodika

52

Číslo periodika v rámci svazku

2-3

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

29

Strana od-do

269-297

Kód UT WoS článku

000351160200008

EID výsledku v databázi Scopus

—