Synthesis of Live Behaviour Models for Fallible Domains

We revisit synthesis of live controllers for event-based operational models. Our technique conforms to the foundational requirements engineering World/Machine model, makes explicit the assumptions on the environment behaviour and distinguishes between controlled and monitored actions. We remove one aspect of an idealized problem domain by allowing to integrate failures of controller actions in the environment model. Classical treatment of failures through strong fairness leads to a very high computational complexity and may be insufficient for many interesting cases. We identify a realistic stronger fairness condition on the behaviour of failures. Furthermore, the resulting controllers exhibit the only possible behavior in face of the given topology of failures: they keep retrying and never give up. We then identify some well-structure conditions on the environment that ensure that the resulting controller will be eager to satisfy its goals. Furthermore, for environments that satisfy these conditions and have an underlying probabilistic behaviour, the measure of traces that satisfy our fairness condition is 1, giving further evidence to the usefulness of this condition.


PDF