TY - GEN
T1 - Modal transition systems
T2 - 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011
AU - Beneš, Nikola
AU - Černá, Ivana
AU - Křetínský, Jan
PY - 2011
Y1 - 2011
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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=80054075398&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-24372-1_17
DO - 10.1007/978-3-642-24372-1_17
M3 - Conference contribution
AN - SCOPUS:80054075398
SN - 9783642243714
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 228
EP - 242
BT - Automated Technology for Verification and Analysis - 9th International Symposium, ATVA 2011, Proceedings
Y2 - 11 October 2011 through 14 October 2011
ER -