Lead-Supervisor:
Co-Supervisors:
In control software, inputs and outputs depend in complex ways on each other and their own previous state. Classical functional specifications thus do not exist; instead, control software is specified by behavioural models, which, when run, simulate the evolution of outputs. Explanations that are useful to (software or human) clients of a control software must reduce its complexity but at the same time also capture its overall behaviour. Our idea is to explain control-theoretic dependencies by reducing system behaviour to appropriately combined abstract functions (``control patterns’’) and providing an executable self-explanation that emulates system evolution in a coarse-grained way.
Desirable background and expertise: Prior exposure to temporal logic or other computational logics, and interest in methods for formal reasoning (e.g., model checking).