Browse Prior Art Database

A Proof System for Dataflow Networks with Indeterminiate Modules

IP.com Disclosure Number: IPCOM000148397D
Original Publication Date: 1986-Sep-30
Included in the Prior Art Database: 2007-Mar-29
Document File: 26 page(s) / 1M

Publishing Venue

Software Patent Institute

Related People

Moitra, Abha: AUTHOR [+3]

Abstract

A Proof System for Dataflow Networks with Indeterminate Modules Abha Moitra P~akash Panangade n TR 86-782 September 1986 Department of Computer Science Cornell University lthaca. NY 14853 A Proof System for Dataflow Networks with Indeterminate Modules Abha Moitra Prakash PanangadenComputer Science Department, Cornell University Abstract In this paper we discuss a model for dataflow networks containing indeterminate operators and the associated proof system. The model is denotational and associates with each network the set of possible behaviors. The possible behaviors are represented by traces. The novel feature of our proof system is that we give an inductive proof rule for recursively defined networks based on a fixed point construction given by Keller and Panangaden. We show soundness and relative completeness of our proof system. I Introduction In this paper we discuss a model for dataflow networks containing inde- terminate operators and the associated proof system. The model that we present is due to Keller and Panangadem [8,7,11]. The model is denota- tional and associates with each network the set of possible behaviors. A possible behavior of the network is represented by the sequence of possible events that occur in a particular execution. Precedence of events in the sequence is interpreted as temporal precedence. This kind of model was suggested by Keller in (61 and was developed further by Brock and Ack- errnan (21 and by Pratt [12]. The novel feature of the model developed by Keller and Panangaden [7] is that a fixed-point construction is given. The model of Brock and Ackerman does not describe how one can combine infinite behaviors. Subsequent proof systems and models, for example that of Nguyen, Gries aod Owicki [lo] present an infinitary proof rule for net- works with loops in them. We present an inductive proof rule based on the fixed-point construction.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 9% of the total text.

Page 1 of 26

A Proof System for Dataflow Networks with Indeterminate Modules

  Abha Moitra P~akash

Panangade n

 TR 86-782
September 1986

Department of Computer Science Cornell University
lthaca. NY 14853

[This page contains 1 picture or other non-text object]

Page 2 of 26

[This page contains 1 picture or other non-text object]

Page 3 of 26

A Proof System for Dataflow Networks with Indeterminate Modules

Abha Moitra

         
Prakash Panangaden
Computer Science Department, Cornell University

Abstract

  In this paper we discuss a model for dataflow networks containing indeterminate operators and the associated proof system. The model is denotational and associates with each network the set of possible behaviors. The possible behaviors are represented by traces. The novel feature of our proof system is that we give an inductive proof rule for recursively defined networks based on a fixed point construction given by Keller and Panangaden. We show soundness and relative completeness of our proof system.

[This page contains 1 picture or other non-text object]

Page 4 of 26

[This page contains 1 picture or other non-text object]

Page 5 of 26

I Introduction

In this paper we discuss a model for dataflow networks containing inde- terminate operators and the associated proof system. The model that we present is due to Keller and Panangadem [8,7,11]. The model is denota- tional and associates with each network the set of possible behaviors. A possible behavior of the network is represented by the sequence of possible events that occur in a particular execution. Precedence of events in the sequence is interpreted as temporal precedence. This kind of model was suggested by Keller in (61 and was developed further by Brock and Ack- errnan (21 and by Pratt [12]. The novel feature of the model developed by Keller and Panangaden [7] is that a fixed-point construction is given. The model of Brock and Ackerman does not describe how one can combine infinite behaviors. Subsequent proof systems and models, for example that of Nguyen, Gries aod Owicki [lo] present an infinitary proof rule for net- works with loops in them. We present an inductive proof rule based on the fixed-point construction.

  It has long been felt that a fixed-point construction was impossible for fair networks containing indeterminate operaton because fairness is not "continuous". Indeed the fixed-point construction that we give does not use standard domain theoretic techniques but instead uses a category t heoretic limit construction. The use of category t heoretic met hods was first proposed by Lehmann 191. Subsequent Xy Abramsky gave a denot ational semantics for unbounded indeterminacy based on category theory (11. The inductive proof rule that we obtain is somewhat complicated since it has to express the fairly complicated limit construction rather than the somew hat simpler least upper bound...