Paper Info
Title
Modal transition systems: composition and LTL model checking
Abstract
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.
Year
DOI
Venue
2011
10.1007/978-3-642-24372-1_17
ATVA
Keywords
Field
DocType
main result,ltl model checking,conjunctive composition problem,modal transition system,disjunctive extension,abstract interpretation,compositional verification,mts composition,common implementation,general incompleteness,refinement,conjunction,model checking
Discrete mathematics,Model checking,EXPTIME,Abstract interpretation,Computer science,P,Algorithm,Linear temporal logic,Theoretical computer science,Conjunctive normal form,Software product line,Modal
Conference
Volume
ISSN
Citations 
6996
0302-9743
20
PageRank 
References 
Authors
0.67
29
3
Name
Order
Citations
PageRank
N. Beneš1423.58
Ivana Černá21379.10
Jan Křetínský319012.05