Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems
This work addresses a limitation in compositional theories for system design, enabling more flexible reasoning about substitutability in complex systems, though it appears incremental by extending existing frameworks.
The paper tackles the problem of feedback composition in systems that are non-deterministic and non-input-receptive, such as partial relations, by proposing a compositional theory using predicate and property transformers with fail and unknown values. It shows that instantaneous feedback for stateless systems and feedback with unit delay for stateful systems preserve refinement relations.
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.