Refinement checking on parametric modal transition systems

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
Refinement checking on parametric modal transition systems
Original language description
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.
Czech name
—
Czech description
—

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

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

Similar results(10)