Curtailing Infinite Stream Behaviours

摘要

Stream processing functions provide an abstract model of communicating components in distributed systems. The finite resp. infinite behaviour of a deterministic component is described by a function on finite resp. on infinite input histories. We present a formal method for refining infinite behaviours to finite behaviours using bound functions at the rear of the stream. We illustrate the approach with two case studies, viz. a shift reg-ister and a synchronization component.