Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems

TL;DR

This paper develops a new compositional feedback theory applicable to non-deterministic and non-input-receptive systems, extending existing theories limited to deterministic or input-receptive systems, and preserving refinement relations.

Contribution

It introduces a novel compositional feedback framework for complex systems using predicate and property transformers, applicable to partial relations with fail and unknown values.

Findings

Defines instantaneous feedback for stateless systems

Introduces feedback with unit delay for stateful systems

Ensures refinement preservation in non-deterministic, non-input-receptive systems

Abstract

Feedback is an essential composition operator in many classes of reactive and other systems. This paper studies feedback in the context of compositional theories with refinement. Such theories allow to reason about systems on a component-by-component basis, and to characterize substitutability as a refinement relation. Although compositional theories of feedback do exist, they are limited either to deterministic systems (functions) or input-receptive systems (total relations). In this work we propose a compositional theory of feedback which applies to non-deterministic and non-input-receptive systems (e.g., partial relations). To achieve this, we use the semantic frameworks of predicate and property transformers, and relations with fail and unknown values. We show how to define instantaneous feedback for stateless systems and feedback with unit delay for stateful systems. Both operations preserve the refinement relation, and both can be applied to non-deterministic and non-input-receptive systems.