The Modal Transition System Control Problem

TitleThe Modal Transition System Control Problem
Publication TypeConference Paper
Year of Publication2012
AuthorsD'Ippolito, N, Braberman, VA, Piterman, N, Uchitel, S
Conference Name18th International Symposium on Formal Methods (FM 2012)
Date Published08/2012
PublisherSpringer Verlag
Conference LocationParis, France
AbstractController synthesis is a well studied problem that attempts to automatically generate an operational behaviour model of the system- to-be such that when deployed in a given domain model that behaves according to specified assumptions satisfies a given goal. A limitation of known controller synthesis techniques is that they require complete descriptions of the problem domain. This is limiting in the context of modern incremental development processes when a fully described prob- lem domain is unavailable, undesirable or uneconomical. In this paper we study the controller synthesis problem when there is partial behaviour information about the problem domain. More specifically, we define and study the controller realisability problem for domains described as Modal Transition Systems (MTS). An MTS is a partial behaviour model that compactly represents a set of complete behaviour models in the form of Labelled Transition Systems (LTS). Given an MTS we ask if all, none or some of the LTS it describes admit an LTS controller that guaran- tees a given property. We show a technique that solves effectively the MTS realisability problem and is in the same complexity class as the corresponding LTS problem.
Refereed DesignationRefereed
Work Package: