Control Synthesis using Modal Logic and Partial Bisimilarity

Allan van Hulst

Promotors: prof.dr. J.C.M. Baeten (CWI and UvA) and prof.dr. W.J. Fokkink (VUA and TU/e)
Copromotor: M.A. Reniers (TU/e)
Technische Universiteit Eindhoven
Date: 6 September, 2016, 16:00


This thesis describes the developments within four years of research into the automated synthesis of controlled systems. The main research question is as follows: given a non-deterministic behavioral description of a system in terms of states and state transitions and given a logical specification of desired behavior, how is it possible to restrict system behavior such that the system conforms to the specification? While deriving a new behavioral description, we require that it conforms to a number of
properties of supervisory control theory. For instance, it is not allowed to forbid accessible uncontrollable behavior (controllability property) and furthermore the behavioral restriction is required to be minimally restrictive. Such research may find applications in the control of manufacturing networks or systems of conveyor belts.

The chosen approach is of formal mathematical nature and based upon an abstract description of the underlying system as a Kripke-model, combined with a specification in modal logic of desired behavior. Part of the performed research is an investigation for which logical specifications this research question is solvable at all. In addition, a precise formulation of the problem to be resolved has been the subject of research. In particular: how to establish a relational connection between the original system and the synthesis result via partial bisimulation. A solution mechanism for a reasonably expressive logical formalism including invariant and reachability formulas has been investigated extensively.

Central issue within the applied methodology are modifications to the transition relation which expresses state transitions. Thereby, state names are coupled to logical expressions which have to be locally valid. Following this step, transitions may be removed based upon a validity approximation of expressions which have been assigned to target states of transitions. Based upon the assumption that the original system is modeled by finitely many transitions, we can prove that that stabilization takes place. This approach has been formally verified during the research and may thereby considered to be valid.

Special attention deserves the research approach via the Coq proof assistant. Using this software it is possible to very precisely verify the validity of mathematical definitions and the proofs based on those. This relates to both the research results and the research path. In the end, there is more certainty about the validity of the obtained results, but significant time was invested into formally establishing mathematical structures and proof steps.

The research within this thesis is closed by a chapter about process algebraic descriptions in relation to the synthesis problem. Using this alternative formalism, expression of the synthesis problem is very well possible, having the additional advantage that equalities make algebraic reasoning about system descriptions more straightforward.