WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:     | 1 |   ...   | 8 | 9 || 11 | 12 |

«A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Electrical Engineering and Computer ...»

-- [ Page 10 ] --

The concept of F -covariety is the coalgebraic counterpart of the concept of F -variety, which is a generalization, in the same sense as before, of the concept of Σ-variety, what Birkhoff called a family of algebras when he introduced the concept in [13]. It is our idea of a “reasonably specified” full subcategory of F -Coalg.

For example, the category of all Abrahamson labelled execution coalgebras, defined in the obvious way, and all homomorphisms between them is a (Pow ◦ Seq ◦ (L × Id))-covariety, as is the category of all generable labelled execution coalgebras and all homomorphisms between them. But we will not need to prove this here.

Just as we did with the notion of finality, we generalize the notion of completeness to full subcategories.

We say that C, γ is complete in S if and only if C, γ is in S, and for every F -coalgebra C, γ in S and any c ∈ C, there is exactly one c ∈ C such that c and c are bisimilar among C, γ and C, γ.

The following is a generalization of Theorem 2.4.13:

CHAPTER 3. EXECUTION SYSTEMS 88

Theorem 3.5.2. For every F -covariety C, the following are true:

(a) C, γ is final in C;

(b) for every small F -coalgebra C, γ in C, there is exactly one homomorphism from C, γ to C, γ ;

(c) C, γ is complete in C;

(d) for every small F -coalgebra C, γ in C, and any c ∈ C, there is exactly one c ∈ C such that c and c are bisimilar among C, γ and C, γ.

Proof. See proof of Theorem 2.4.13.

The reason that we were able to reuse the proof of Theorem 2.4.13 here without any modification or adjustment is that, because of the closure properties of an F -covariety, all relevant constructions in that proof can be carried out inside C. The only structures in that proof that are not necessarily in C are the bisimulations, which are not supposed to either.

The following is a generalization of Theorem 2.5.1:

Theorem 3.5.

3. For every F -covariety C, there is an F -coalgebra that is final in C.

Proof. Assume an F -covariety C.

Let C, γ be an F -coalgebra that is final in F -Coalg.

Let C, γ be a direct sum of all small F -coalgebras in C.

Let h be the unique homomorphism from C, γ to C, γ.

Then, by Theorem 2.4.5, there is a class function ρ : ran h → F (ran h) such that

–  –  –

Let ι be the canonical injection map from C to C.

Then h ◦ ι is a homomorphism from C, γ to ran h, ρ.

Suppose, toward contradiction, that there are homomorphisms h1 and h2 from C, γ to ran h, ρ such that

–  –  –

contrary to C, γ being final in F -Coalg.

Therefore, there is at most one homomorphism from C, γ to ran h, ρ.

Thus, there is exactly one homomorphism, namely h ◦ ι, from C, γ to ran h, ρ.

Thus, by generalization and Theorem 3.5.2, ran h, ρ is final in C.

Theorem 3.5.

3 is easy enough to be already known. But being unable to trace it in the literature, we have taken care to prove it here (but see [3, thm 2.2]).

3.6 Execution systems in the literature The process algebra literature is dominated by the concept of labelled transition system.

And to some extent, this is understandable. For process algebra emerged from a marriage of Plotkin’s structural operational semantics (see [48]), and Keller’s named transition systems (see [32]) (see [41, chap. 12], [12], [49], and [10]). This marriage was the work of Robin Milner, and is most clearly expounded in [41], but was already present in [36], where the so-called expansion law was stated for the first time.

The expansion law has been a constant source of controversy in the theory of concurrency.

In the language of Milner’s CCS (see [40], [41]), a typical equation asserted by the law is

the following:

a.0 | b.0 = a.b.0 + b.a.0.

Here, ‘a’ and ‘b’ stand for arbitrary actions, ‘0’ for the inactive agent, which is incapable of performing any action, ‘.’ for sequential composition, ‘|’ for parallel composition, and ‘+’ for alternative composition. Thus, the intended meaning of the equation is that the parallel CHAPTER 3. EXECUTION SYSTEMS 90 execution of a and b is “equivalent”, in some sense, to the indeterminate serialization of the two.

In order to justify the expansion law, and the blurring between causal dependence and

temporal precedence resulting from it, Milner wrote the following in [36, p. 81]:

We do not yet know how to frame a sufficiently general law without, in a sense, explicating parallelism in terms of non-determinism. More precisely, this means that we explicate a (parallel) composition by presenting all serializations - or interleavings - of its possible atomic actions. This has the disadvantage that we lose distinction between causally necessary sequence, and sequence which is fictitiously imposed upon causally independent actions; [... ]. However, it may be justified to ignore it if we can accept the view that, in observing (communicating with) a composite system, we make our observations in a definite time sequence, thereby causing a sequencing of actions which, for the system itself, are causally independent.





Effectively, what he argued for was a dichotomy between causation and observation in the theory of concurrency. And what he proposed as an observational view to the theory was the interleaving of the atomic actions of the various agents inside a system as would be perceived by a single, sequential observer outside the system. But what he failed to recognize was that the expansion law is in fact inconsistent with that view.

To understand the mismatch, consider the following equation derived from the expansion

law, again in the language of CCS:

fix(X = a.X) | fix(X = b.X) = fix(X = a.X + b.X).

Here, we use recursion expressions to define agents with infinite behaviour. Thus, fix(X = a.X) is an agent that forever iterates a, fix(X = b.X) one that forever iterates b, and fix(X = a.X + b.X) one that at each iteration, does either a or b, indeterminately choosing between the two. But whereas every infinite sequence over {a, b} is a trace of a possible execution of fix(X = a.X + b.X), not every such sequence is consistent with what could be perceived by a sequential observer of fix(X = a.X) | fix(X = b.X). Indeed, only those sequences that contain an infinite number of a’s and an infinite number of b’s are.

For if fix(X = a.X) and fix(X = b.X) execute in parallel, each of them must eventually perform an infinite number of actions, and each of these actions must eventually be perceived by any sequential observer of fix(X = a.X) | fix(X = b.X).

All this goes unnoticed in the finite case, because interleaving the executions of two finite agents is ultimately equivalent to indeterminately alternating between the two. But the expansion law blindly carried that equivalence over to the infinite case. And this created CHAPTER 3. EXECUTION SYSTEMS 91 confusion. The word “interleaving” became synonymous to the word “indeterminate”, and the observational view was robbed of its power to express liveness properties such as finite delay or termination.

Of course, it is not the expansion law per se that is to blame for this confusion.

Interleaving is an operation on executions, not transitions, and the use of labelled transition systems was always going to cause problems with it. But instead of replacing transitions with executions in their systems, people started augmenting them with all kinds of different pieces of information that would allow them to distinguish the “admissible” sequences of transitions from the “inadmissible” ones. And more often than not, the result was a type of modelling structure that could no longer claim adherence to the observational view. The few attempts that did use executions directly, at least those that we are aware of (see [18], [17]), were not concerned with organizing them into structures and looking at their branching properties, and anyway, seem to have received only scant attention, possibly due to their poor presentation.

The first place where we do see executions organized into structures is not process algebra, but temporal logic. These so-called path structures (see Section 3.1) are quite popular in the beginning. We do not see a formal concept of bisimulation for them, but there is definitely interest in their branching properties. The notions of suffix, fusion, and limit closure are all defined in connection with path structures. Eventually, they give way to Kripke structures, inherited from modal logic, and claimed to provide “a setting more appropriate to concurrency” (see [21, p. 152]). They do not. But despite the voices of reason asking for a separation between implementation and correctness issues in reasoning about concurrent programs (for example, see [16]), transitions remain in the lead role.

In [26], Hennessy and Stirling introduce what appears to be the first type of labelled execution system in the literature. They call systems of that type general transition systems, and in their definition, demand not only suffix and fusion closure, but prefix closure as well, with the justification that it “also appears to be natural” (see [26, p. 27]).

They also define a concept of extended bisimulation for such systems, which is basically the same as our formally derived concept of bisimulation between labelled executions systems (see Definition 3.2.3). The focus in [26] is in logic, and specifically, in a generalization of Hennessy-Milner Logic (see [25]) to general transition systems. But what is surprising is that no attempt is later made to apply the ideas of general transition systems and extended bisimulations to the semantics of processes.

More than ten years later, these ideas pop up in a “very rough and incomplete draft” of Aczel (see [4]), who is aware of Hennessy’s work in [24], a precursor of [26], but apparently, unaware of the work in [26] (see footnote in [4, p. 3]). Aczel’s intention is to apply the final universe approach of [3] to the semantics of Milner’s SCCS with finite delay (see [38]). But his execution is indeed “very rough and incomplete”. The proposed type of structure is a generalized type of labelled transition system, where each state is equipped with the set of CHAPTER 3. EXECUTION SYSTEMS 92 all infinite sequences of transitions “admissible” from that state. An added condition of “stability” makes structures of that type ultimately equivalent to the general transition systems of [26], but only because the latter are prefix closed. Eventually, these structures are represented as coalgebras over Class, and [3, thm. 2.2] is used to prove the existence of a final coalgebra in the full subcategory of all such coalgebras that are “stable”.

The only other place where we find these ideas applied to the semantics of processes is [27].

The starting point is again Milner’s SCCS with finite delay, and the structures used are practically the same as in [4]. But the approach is purely categorical. Indeed, the main goal in [27] is showing how much can be done within category theory alone. Apparently, a lot, but not without cost.

Comparing [26], [4], and [27] with our work here, there are two things that we think stand out and would like to mention.

First, as regards the general idea underlying the concept of labelled execution system, we find that in all three of [26], [4], and [27], the notion of indeterminate termination, and its use in modelling the behaviour of reactive systems, has been completely overlooked. This is easy to put right in [26], where prefix closure is an added feature, but not so in [4] and [27], where the property is practically built into the structure of a system.

Second, as regards the formalization of the idea, we believe that the present approach represents a great simplification, both conceptually and notationally, over what was done in all three of [26], [4], and [27], and hope that the reader will appreciate the power and elegance of our framework, which, we think, are felt in every part of the theory.

It should be emphasized that the precedence of [26], [4], and [27] over our work here is not causal, only temporal. Our ideas were developed, and for the most part, worked out before any acquaintance with these studies. The above review was mainly driven by our curiosity to understand why ideas that in retrospect seem so natural have not found their way into the household of the average concurrency theorist.

In the end, one can only speculate. But one thing is certain: if matters of pedagogy have played any role in this, transition semantics have definitely profited from it; for people like pictures, and execution systems are impossible to draw.

Chapter 4 Sequential Asynchronous Processes

4.1 Our intuitive notion of asynchronous process What is a process? This is a question that has troubled concurrency theorists ever since the birth of the field almost fifty year ago. And yet, there is still very little agreement as to what the answer is. With the advent of process algebra in the eighties came the well known controversy between so-called true concurrency and interleaving semantics, adding another dimension to the problem.

The central figure in this controversy was of course Robin Milner, who, as we have seen, was the one to argue for the dichotomy between causation and observation, which can be tersely described as the difference between events partially ordered by causal dependence, and actions totally ordered by temporal precedence (see [9]). Milner’s idea was nothing less than brilliant. But it was marred by the inadequacies of the used model, the labelled transition system.

Our work thus far has been to fix just that. And we have done so by introducing a model that we believe can do justice to the interleaving approach. We now want to use this model to define an abstract notion of asynchronous process.



Pages:     | 1 |   ...   | 8 | 9 || 11 | 12 |


Similar works:

«DEEP IN THE BURBS by STEVE THOMASON A Thesis Proposal Submitted to the Faculty of Luther Seminary In Partial Fulfillment of The Requirements for the Degree of DOCTOR OF PHILOSOPHY ST. PAUL, MINNESOTA SECTION ONE RESEARCH QUESTION The Question What do suburbia and spirituality have in common? The term suburbia often conjures up caricatured images of plastic, white, middle-class Americans driving gasguzzling Sport Utility Vehicles past white picket fences into cavernous garages that swallow them...»

«WRITING BARCELONA: REFLECTIONS ON CITY PLANNING AND URBAN EXPERIENCE, 1854-1888 BY JORDI OLIVAR DISSERTATION Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Spanish in the Graduate College of the University of Illinois at Urbana-Champaign, 2010 Urbana, Illinois Doctoral Committee: Associate Professor Luisa-Elena Delgado, Chair Associate Professor Jordana Mendelson, New York University Associate Professor Joyce Tolliver Assistant Professor Ericka...»

«Theory into Practice in Environmental Education: Towards an evidence-based approach Submitted by Junko Katayama For the Degree of Doctor of Philosophy From the University of Bath Department of Education April 2009 COPYRIGHT Attention is drawn to the fact that copyright of this thesis rests with its author. This copy of the thesis consults it is understood to recognise that its quotation from the thesis and no information derived from it may be published without the prior written consent of the...»

«Roam: A Scalable Replication System for Mobile and Distributed Computing David Howard Ratner University of California, Los Angeles January, 1998 A dissertation submitted in partial satisfaction of the requirements for the degree Doctor of Philosophy in Computer Science UCLA Computer Science Department Technical Report UCLA-CSD-970044 Thesis committee: Gerald J. Popek, co-chair W. W. Chu, co-chair Eli Gafni Mario Gerla Donald Morisky c Copyright by David Howard Ratner To my father Robert, my...»

«The Present Participle as a Marker of Style and Authorship in Old English Biblical Translation by George James McBeath Lamont A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Centre for Medieval Studies University of Toronto © Copyright by George James McBeath Lamont 2015 The Present Participle as a Marker of Style and Authorship in Old English Biblical Translation George James McBeath Lamont Doctor of Philosophy Centre for Medieval Studies...»

«NORTHWESTERN UNIVERSITY NUMERAL CLASSIFIERS AND THE STRUCTURE OF DP A DISSERTATION SUBMITTED TO THE GRADUATE SCHOOL IN PARTIAL FULFILLMENT OF THE REQUIREMENTS for the degree DOCTOR OF PHILOSOPHY Field of Linguistics By Lewis Gebhardt EVANSTON, ILLINOIS June 2009 ABSTRACT Numeral Classifiers and the Structure of DP Lewis Gebhardt This dissertation investigates the structure of the Determiner Phrase from a crosslinguistic perspective, with a particular focus on English and Persian. Three main...»

«New Techniques for Out-Of-Core Visualization of Large Datasets ˆ Wagner Toledo Correa A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy Recommended for Acceptance by the Program in Computer Science January 2004 c Copyright by Wagner Toledo Corrˆa, 2004. e All Rights Reserved Abstract We present a practical system to visualize large datasets interactively on commodity PCs. Interactive visualization has applications in many...»

«LOOP OPTIMIZATION TECHNIQUES ON MULTI-ISSUE ARCHITECTURES by Dan Richard Kaiser A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Computer and Communication Sciences) in The University of Michigan Doctoral Committee: Professor Trevor N. Mudge, Chair Associate Professor Richard B. Brown Professor Edward S. Davidson Professor Ronald J. Lomax Associate Professor Karem A. Sakallah © Dan Richard Kaiser 1994 All Rights Reserved Dedicated to...»

«THE WIND RESISTANCE OF ASPHALT ROOFING SHINGLES By CRAIG ROBERT DIXON A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY UNIVERSITY OF FLORIDA © 2013 Craig Robert Dixon To my Mom ACKNOWLEDGMENTS First and foremost, I would like to thank my advisors, Drs. David O. Prevatt, Forrest J. Masters, and Kurtis R. Gurley for their guidance, support, and friendship. This work would not have been...»

«FRACTIONAL-N SYNTHESIZER ARCHITECTURES WITH DIGITAL PHASE DETECTION by Mark A. Ferriss A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Electrical Engineering) in The University of Michigan Doctoral Committee: Professor Michael Flynn, Chair Professor Dennis M. Sylvester Assistant Professor Jerome P. Lynch Assistant Professor David D. Wentzloff © Mark A. Ferriss ACKNOWLEDGENTS Thanks Everyone! Firstly, I would like to thank my advisor,...»

«CICERO’S IDEAL STATESMAN IN THEORY AND PRACTICE By JONATHAN PETER ZARECKI A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY UNIVERSITY OF FLORIDA 2005 Copyright 2005 by Jonathan Peter Zarecki MEAE CARISSIMAE REBECCAE ACKNOWLEDGMENTS Numerous people deserve mention for their help in the completion of this dissertation. First and foremost, I would like to thank my committee chair, Prof....»

«Command Hallucinations and the Risk of Violence and Self-Harm: What distinguishes compliers from non-compliers? Elizabeth Andrew Thesis submitted for the degree of Doctor of Philosophy Cardiff University 2010 UMI Number: U584482 All rights reserved INFORMATION TO ALL USERS The quality of this reproduction is dependent upon the quality of the copy submitted. In the unlikely event that the author did not send a complete manuscript and there are missing pages, these will be noted. Also, if...»





 
<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.