Process Algebra for Modal Transition Systemses

by Nikola Beneš, Jan Křetínský, A full version of the paper presented at MEMICS 2010. September 2010, 15 pages.

FIMU-RS-2010-11. Available as Postscript, PDF.


The formalism of modal transition systems (MTS) is a well established framework for systems specification as well as abstract interpretation. Nevertheless, due to incapability to capture some useful features, various extensions have been studied, such as e.g. mixed transition systems or disjunctive MTS. Thus a need to compare them has emerged. Therefore, we introduce transition systems with obligations as a general model encompassing all the aforementioned models, and equip it with a process algebra description. Using these instruments, we then compare the previously studied subclasses and characterize their relationships.