On Refinements of Boolean and Parametric Modal Transition Systems

Abstract. We consider the extensions of modal transition systems (MTS), namely Boolean MTS and parametric MTS and we investigate the re-finement problems over both classes. Firstly, we reduce the problem of modal refinement over both classes to a problem solvable by a QBF solver and provide experimental results showing our technique scales well. Sec-ondly, we extend the algorithm for thorough refinement of MTS provid-ing better complexity then via reductions to previously studied problems. Finally, we investigate the relationship between modal and thorough re-finement on the two classes and show how the thorough refinement can be approximated by the modal refinement.