A Decision Method for Elementary Stream Calculus

TL;DR

The paper addresses the challenge of solving quantified constraints over streams, which are inherently second-order when expressed over sequences. It introduces a doubly exponential decision procedure for the first-order equality theory of real-valued streams by modeling streams as formal Laurent series and applying quantifier elimination in real-closed fields, with definitional extensions for shift, rational, and automatic stream constructs. Key contributions include a rigorous real-closedness and IVP framework for streams, a principled decision procedure, and a set of definitional encodings that enable reasoning about stream circuits, heads/tails, and bisimulations within a decidable theory. The work lays a foundation for automated analysis of elementary stream calculus and has potential implications for verifiable design of stream-based systems and controllers, though practical efficiency remains an area for further development.

Abstract

The main result is a doubly exponential decision procedure for the first-order equality theory of streams with both arithmetic and control-oriented stream operations. This stream logic is expressive for elementary problems of stream calculus.

Figures (2)

• Figure 1: Finite Stream Circuit.
• Figure 2: Commuting Stream Embeddings (${\mathcal{K}}$ is a field or at least an integral domain, $*$ denotes completion for valuation $|.|$, and $/$ the fraction field construction.

Theorems & Definitions (21)

• remark 1
• remark 2
• proposition 1
• proposition 2
• proposition 3
• proposition 4
• proof
• remark 3
• lemma 1: IVP
• proof