Automated Controller Synthesis for non-Deterministic Piecewise-Affine Hybrid Systems

To further advance space based science the need for ever more precise measurement techniques
increases. One of the most promising new ideas are satellite formations where
accurate spatial control of multiple spacecraft can be used to create very large virtual
apertures or very sensitive interferometric measurements.
Control of satellite formations presents a whole new set of challenges for spacecraft
control systems requiring advances in actuation, sensing, communication, and control
algorithms. Specifically having the control system duplicated onto multiple satellites increases
the possibility of negating faults while the added number of components increases
the likelihood of faults occurring. Combined with the fact that once a mission is launched
it is prohibitively expensive to repair a failing component there is a good case for designing
fault tolerant controllers specifically for satellite formations.
This thesis uses a hybrid systems model of a satellite formation with possible actuator
faults as a motivating example for developing an automated control synthesis method for
non-deterministic piecewise-affine hybrid systems (PAHS). The method does not only
open an avenue for further research in fault tolerant satellite formation control, but can be
used to synthesise controllers for a wide range of systems where external events can alter
the system dynamics.
The synthesis method relies on abstracting the hybrid system into a discrete game,
finding a winning strategy for the game meeting a computational tree logic formula and
refining the resulting solution to a catalogue of piecewise-affine controllers.
The method has been implemented as aMatlab toolbox, PAHSCTRL , using linear matrix
inequality feasibility computations for finding the discrete abstraction, UppAal Tiga
for solving the discrete game and linear optimisation solvers for controller refinement.
To illustrate the efficacy of the method a reoccurring satellite formation example including
actuator faults has been used. The end result is the application of PAHSCTRL on
the example showing synthesis and simulation of a fault tolerant formation controller.
The presented method has some limitations. It relies on full state observations and
can thus not handle sensor system faults and the computational complexity of computing
discrete abstractions grows exponentially with the dimension of the state space. The
latter limitation is mitigated by the fact that the computations are performed off-line and
the computation time scales almost linearly with the number of parallel execution units.
Finally, most realistic system models must undergo a transformation to be brought on
PAHS form and this usually involves partitioning the state space of the different failure
mode into polytopes. Experience shows that the specific partitioning of the state space
can have profound effects on the discrete game abstraction and further research is therefore
needed into partitioning methods in order to make the proposed synthesis method
generally applicable.