Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Solving Causal Stream Inclusions

Harald Ruess

TL;DR

The fixpoint approximation provides an anytime algorithm with which finite prefixes of solutions can be calculated and is illustrated for some central concepts of system design.

Abstract

We study solutions to systems of stream inclusions of the form 'f in T(f)', where the nondeterministic transformer 'T' on omega-infinite streams is assumed to be causal in the sense that elements in output streams are determined by a finite prefix of inputs. We first establish a correspondence between logic-based causality and metric-based contraction. Based on this causality-contraction connection we then apply fixpoint principles to the spherically complete ultrametric space of streams to construct solutions of stream inclusions. The underlying fixpoint iterations induce fixpoint induction principles to reason about these solutions.In addition, the fixpoint approximation provides an anytime algorithm with which finite prefixes of solutions can be calculated. These developments are illustrated for some central concepts of system design.

Solving Causal Stream Inclusions

TL;DR

The fixpoint approximation provides an anytime algorithm with which finite prefixes of solutions can be calculated and is illustrated for some central concepts of system design.

Abstract

We study solutions to systems of stream inclusions of the form 'f in T(f)', where the nondeterministic transformer 'T' on omega-infinite streams is assumed to be causal in the sense that elements in output streams are determined by a finite prefix of inputs. We first establish a correspondence between logic-based causality and metric-based contraction. Based on this causality-contraction connection we then apply fixpoint principles to the spherically complete ultrametric space of streams to construct solutions of stream inclusions. The underlying fixpoint iterations induce fixpoint induction principles to reason about these solutions.In addition, the fixpoint approximation provides an anytime algorithm with which finite prefixes of solutions can be calculated. These developments are illustrated for some central concepts of system design.
Paper Structure (22 sections, 30 theorems, 40 equations, 1 figure)

This paper contains 22 sections, 30 theorems, 40 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Streams
  4. Transformers
  5. Composing Transformers.
  6. Refinement.
  7. Causality
  8. Mealy Realizability.
  9. Composition.
  10. Fixpoints.
  11. Contraction
  12. Multivalued Contraction
  13. Fixpoints of Stream Transformers
  14. Lipschitz Contraction
  15. Fixpoints
  16. ...and 7 more sections

Key Result

proposition 1

If $(M, d)$ is ultrametric then $({\mathrm{CB}({M})}, \mathcal{H}_{d})$ is also ultrametric.

Figures (1)

  • Figure 1: Finite Stream Circuit.

Theorems & Definitions (45)

  • proposition 1
  • proposition 2: (dieudonne2011foundations, p. 59
  • proposition 3
  • lemma 1
  • lemma 2
  • definition 1: Stream Transformers
  • definition 2
  • lemma 3: Compatibility
  • definition 3: Causal Stream Transformers
  • proposition 4
  • ...and 35 more