On Refinements of Boolean and Parametric Modal Transition Systems

TL;DR

This paper explores extensions of modal transition systems, introduces QBF-based techniques for refinement problems, improves algorithms for thorough refinement, and analyzes relationships between modal and thorough refinement.

Contribution

It presents a QBF-based approach for refinement problems, enhances algorithms for thorough refinement, and studies the connection between modal and thorough refinement in Boolean and parametric MTS.

Findings

QBF-based refinement solving scales well

Improved algorithms for thorough refinement

Thorough refinement can be approximated by modal refinement

Abstract

We consider the extensions of modal transition systems (MTS), namely Boolean MTS and parametric MTS and we investigate the refinement 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. Secondly, we extend the algorithm for thorough refinement of MTS providing better complexity then via reductions to previously studied problems. Finally, we investigate the relationship between modal and thorough refinement on the two classes and show how the thorough refinement can be approximated by the modal refinement.