Modelling a Guardrail for an AI Control System Using CSP

I consider the problem of attempting to constrain the behaviour of artificial intelligence software to prevent it from carrying out unwanted, dangerous, or malicious operations. I shall analyse a medical appliance scenario: the artificial pancreas. I shall model a diabetes patient as a system which contains a certain level of insulin and a certain level of glucose at any given point in time, and may be engaged in eating, rest, or exercise. Sugar levels will be lowered using up some insulin. Exercise will also contribute to lowering sugar levels. The artificial pancreas will periodically inject some more insulin into the patient depending on decisions made by an AI-driven control system when it is provided with monitoring data and it is intended to learn over time how best to manage the patient’s glucose levels. There is also a safety system which may decide to suspend the AI system and trigger a manual or algorithmic override should a particular threshold be breached. I shall use the CSP process algebra to represent the processes and the associated FDR proof tool to deduce properties about their behaviour.