The Modal Transition System Control Problem
Title | The Modal Transition System Control Problem |
Publication Type | Conference Paper |
Year of Publication | 2012 |
Authors | D'Ippolito, N, Braberman, VA, Piterman, N, Uchitel, S |
Conference Name | 18th International Symposium on Formal Methods (FM 2012) |
Date Published | 08/2012 |
Publisher | Springer Verlag |
Conference Location | Paris, France |
Abstract | Controller 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. |
URL | http://publicaciones.dc.uba.ar/Publications/2012/DBPU12a |
Refereed Designation | Refereed |
PDF (Full text):
Work Package:
WP4