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

Viorel Preoteasa, Stavros Tripakis

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

7 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationLICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
PublisherACM
Pages768-777
Number of pages10
ISBN (Electronic)978-1-4503-4391-6
DOIs
Publication statusPublished - 2016
MoE publication typeA4 Article in a conference publication
EventAnnual ACM/IEEE Symposium on Logic in Computer Science - New York, United States
Duration: 5 Jul 20168 Jul 2016
Conference number: 31

Conference

ConferenceAnnual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS
CountryUnited States
CityNew York
Period05/07/201608/07/2016

Fingerprint Dive into the research topics of 'Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems'. Together they form a unique fingerprint.

  • Cite this

    Preoteasa, V., & Tripakis, S. (2016). Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. In LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 768-777). ACM. https://doi.org/10.1145/2933575.2934503