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

DOI10.1145/2933575.2934503MaRDI QIDQ4635940zbMATH OpenOpenAlexFDO

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)

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

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)

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.

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

Cited in

(3)

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

Describes a project that uses

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)