| 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. |
Other formats:
BibTeX
LaTeX
RIS
@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.
|
