Refinement checking on parametric modal transition systems

J 2015

Refinement checking on parametric modal transition systems

BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN, Mikael H. MOLLER, Salomon SICKERT et. al.

Základní údaje

Originální název

Refinement checking on parametric modal transition systems

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí), Kim G. LARSEN (208 Dánsko), Mikael H. MOLLER (208 Dánsko), Salomon SICKERT (276 Německo) a Jiří SRBA (203 Česká republika, domácí)

Vydání

Acta Informatica, Springer, 2015, 0001-5903

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Impakt faktor

Impact factor: 0.722

Kód RIV

RIV/00216224:14330/15:00080734

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1007/s00236-015-0215-4

UT WoS

000351160200008

Klíčová slova anglicky

modal transition systems; refinement; specification; logic

Štítky

formela-journal

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 6. 5. 2015 22:48, RNDr. Nikola Beneš, Ph.D.

Anotace

V originále

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 of the 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. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.

Návaznosti

EE2.3.30.0009, projekt VaV

Název: Zaměstnáním čerstvých absolventů doktorského studia k vědecké excelenci

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

Citovat

BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN, Mikael H. MOLLER, Salomon SICKERT a Jiří SRBA. Refinement checking on parametric modal transition systems. Acta Informatica. Springer, 2015, roč. 52, 2-3, s. 269-297. ISSN 0001-5903. Dostupné z: https://dx.doi.org/10.1007/s00236-015-0215-4.

@article{1232561,
   author = {Beneš, Nikola and Křetínský, Jan and Larsen, Kim G. and Moller, Mikael H. and Sickert, Salomon and Srba, Jiří},
   article_number = {2-3},
   doi = {http://dx.doi.org/10.1007/s00236-015-0215-4},
   keywords = {modal transition systems; refinement; specification; logic},
   language = {eng},
   issn = {0001-5903},
   journal = {Acta Informatica},
   title = {Refinement checking on parametric modal transition systems},
   volume = {52},
   year = {2015}
}

TY  - JOUR
ID  - 1232561
AU  - Beneš, Nikola - Křetínský, Jan - Larsen, Kim G. - Moller, Mikael H. - Sickert, Salomon - Srba, Jiří
PY  - 2015
TI  - Refinement checking on parametric modal transition systems
JF  - Acta Informatica
VL  - 52
IS  - 2-3
SP  - 269-297
EP  - 269-297
PB  - Springer
SN  - 00015903
KW  - modal transition systems
KW  - refinement
KW  - specification
KW  - logic
N2  - 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 of the 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. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.
ER  -

BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN, Mikael H. MOLLER, Salomon SICKERT a Jiří SRBA. Refinement checking on parametric modal transition systems. \textit{Acta Informatica}. Springer, 2015, roč.~52, 2-3, s.~269-297. ISSN~0001-5903. Dostupné z: https://dx.doi.org/10.1007/s00236-015-0215-4.

Podrobný výpis o publikaci