Towards compositional feedback in non-deterministic and non-input-receptive systems

DOI10.1145/2933575.2934503zbMATH Open1401.68013arXiv1510.06379OpenAlexW2239495252MaRDI QIDQ4635940FDOQ4635940

Authors: Viorel Preoteasa, Stavros Tripakis 

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1510.06379

Recommendations

• Feedback in synchronous relational interfaces
• Compositional refinement of interactive systems
• Specification transformers: a predicate transformer approach to composition
• scientific article; zbMATH DE number 2087508
• The refinement calculus of reactive systems

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07) Semantics in the theory of computing (68Q55)

Cited In (3)

• The refinement calculus of reactive systems
• Zero principles for implicit feedback systems
• Compositional assume-guarantee reasoning of control law diagrams using UTP

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: Towards compositional feedback in non-deterministic and non-input-receptive systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635940)