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.

Basic information

Original name

Refinement checking on parametric modal transition systems

Authors

BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution), Kim G. LARSEN (208 Denmark), Mikael H. MOLLER (208 Denmark), Salomon SICKERT (276 Germany) and Jiří SRBA (203 Czech Republic, belonging to the institution)

Edition

Acta Informatica, Springer, 2015, 0001-5903

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Impact factor

Impact factor: 0.722

RIV identification code

RIV/00216224:14330/15:00080734

Organization unit

Faculty of Informatics

DOI

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

UT WoS

000351160200008

Keywords in English

modal transition systems; refinement; specification; logic

Abstract

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.

Links

EE2.3.30.0009, research and development project

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

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

Citovat

BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN, Mikael H. MOLLER, Salomon SICKERT and Jiří SRBA. Refinement checking on parametric modal transition systems. Acta Informatica. Springer, 2015, vol. 52, 2-3, p. 269-297. ISSN 0001-5903. Available from: 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 and Jiří SRBA. Refinement checking on parametric modal transition systems. \textit{Acta Informatica}. Springer, 2015, vol.~52, 2-3, p.~269-297. ISSN~0001-5903. Available from: https://dx.doi.org/10.1007/s00236-015-0215-4.

Detailed Information on Publication Record