Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{950140,
author = {Beneš, Nikola and Černá, Ivana and Křetínský, Jan},
address = {Heidelberg Dordrecht London New York},
booktitle = {ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium},
keywords = {modal transition systems; model checking; refinement; conjunction},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Heidelberg Dordrecht London New York},
isbn = {978-3-642-24371-4},
pages = {228-242},
publisher = {Springer},
title = {Modal Transition Systems: Composition and LTL Model Checking},
year = {2011}
}
TY - JOUR
ID - 950140
AU - Beneš, Nikola - Černá, Ivana - Křetínský, Jan
PY - 2011
TI - Modal Transition Systems: Composition and LTL Model Checking
PB - Springer
CY - Heidelberg Dordrecht London New York
SN - 9783642243714
KW - modal transition systems
KW - model checking
KW - refinement
KW - conjunction
N2 - Modal transition systems (MTS) is a~well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we provide algorithms showing that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we identify an error in a~previous attempt at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition. Secondly, we give a~solution to the common implementation and conjunctive composition problems lowering the complexity from EXPTIME to PTIME.
ER -
BENEŠ, Nikola, Ivana ČERNÁ a Jan KŘETÍNSKÝ. Modal Transition Systems: Composition and LTL Model Checking. In \textit{ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium}. Heidelberg Dordrecht London New York: Springer. s.~228-242. ISBN~978-3-642-24371-4. 2011.
|
