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

<< HOME
CONTACTS

Pages:     | 1 |   ...   | 6 | 7 || 9 | 10 |   ...   | 12 |

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

-- [ Page 8 ] --

In [20], Emerson called a set of paths limit closed provided that for every inﬁnite, strictly increasing chain of ﬁnite preﬁxes of paths in the set, the limit of that chain, in the standard topology of sequences, is again a path in the set. This property was apparently also ﬁrst considered in [1]. But it was Emerson in [20] who proved the independence of all three closure properties, and the equivalence of their conjunction to the existence of a transition relation generating the given set of paths. Apart from the absence of labels, which has no bearing in this particular discussion, Emerson’s setup was diﬀerent in that paths were always inﬁnite. But this too is of no importance in our examples, which, in light of Emerson’s result, appear to implicate violation of limit closure in the failure of the underlying labelled transition system to subsume all the branching information relevant to a given Abrahamson system.

Our next example is perhaps the most curious one.

Consider the simple {l}-labelled transition system portrayed in the following diagram:

–  –  –

There are exactly three Abrahamson {l}-labelled execution systems that one can lay over this labelled transition system. The ﬁrst is the one whose only execution corresponds to the only inﬁnite path in the diagram. The second is the one whose executions correspond to all ﬁnite paths in the diagram. And of course, the third is the one whose executions are all executions of the ﬁrst and second system. But s is not bisimilar with itself among any two of the three.

Informally, the second system is not limit closed, and this is one part of the problem. But the ﬁrst and third are, and so there must be something more going on here. The answer is in the diﬀerence between Emerson’s setup and ours mentioned earlier. Here, executions are not always inﬁnite. In a system that is, informally, suﬃx closed, if there is a ﬁnite execution, then there is an empty execution. And an empty execution creates a type of branching that is impossible to mimic in a labelled transition system.

In an Abrahamson system that is used to model the behaviour of a process, an empty execution can be used to model termination. But if there is another, non-empty execution starting from the same state, then termination becomes a branching choice, one that does not show up in the “possible next step” relation of the system. This feature of indeterminate termination, as we might call it, can seem a little odd at ﬁrst, but is really a highly versatile mechanism, particularly useful in modelling idling in absence of input stimuli, as we shall see in the next chapter.

CHAPTER 3. EXECUTION SYSTEMS 66

Finally, consider the labelled transition system of the following, trivial diagram:

–  –  –

There are exactly two labelled execution systems that one can lay over this labelled transition system: one that has one execution, the empty execution, and one that has no execution. And of course, s is not bisimilar with itself among the two.

This degenerate case deserves little comment. We only remark that in a suﬃx closed system, if a state has no execution starting from it, then it has no execution going through it.

At this point, we have found ﬁve possible causes of failure for the converse of Proposition 3.3.4. We have chosen our examples carefully, to examine each of the ﬁve separately and independently from one another. And we have observed how each of the ﬁrst three connects to violation of one of the three closure properties that have been shown to collectively characterize sets of inﬁnite paths generable by a transition relation. But ﬁnite paths add another dimension to the problem, rendering Emerson’s characterization result obsolete. What we will show next is that impossibility of indeterminate termination, along with a non-triviality condition guarding against the occurrence of an isolated state, can be added to the conditions of suﬃx, fusion, and limit closure, to produce a complete characterization of system generability, insensitive to the length of the executions.

First, we need to make the notion of generability precise. For generality, we transfer ourselves again to the coalgebra side of the theory.

Assume a class function τ : C → Pow(L × C).

Assume c ∈ C.

Assume e ∈ Seq(L × C).

We say that e is a τ -orbit of c if and only if the following are true:

(i) one of the following is true:

–  –  –

Here again, it is the computational interpretation that is most helpful. If we think of τ as a representation of the control ﬂow graph of a possibly indeterminate sequential program, then a τ -orbit of c corresponds to a total execution of that program starting from the node represented by c.

Now, we would like to say that a class function from C to Pow Seq(L × C)) is generated by τ just as long as it assigns to any c ∈ C the set of all τ -orbits of c. But ﬁrst, we need to make sure that this really is a set, and not a proper class.

We write Wτ (c) for a class function from ω to Pow(L × C) such that

–  –  –

We think of Wτ (c) as a wave emitted by c, and propagating through L × C according to τ, and Wτ (c)(n) as the wavefront at the nth time instance.

Proposition 3.4.1. If e is a τ -orbit of c, then for every n ∈ ω, if tailn e =, then head tailn e ∈ Wτ (c)(n).

Proof. We use induction.

If n = 0, then tailn e = e. Thus, if tailn e =, then there is l, c, and e such that l, c ∈ τ (c) and

–  –  –

Proposition 3.4.2. For every n ∈ ω, Wτ (c)(n) is a set.

Proof. We use induction.

If n = 0, then Wτ (c)(n) = τ (c), which, by deﬁnition of Pow, is a set.

Otherwise, there is m ∈ ω such that n = m + 1. By the induction hypothesis, Wτ (c)(m) is a set. Then clearly, Wτ (c)(m + 1) is a set, and so Wτ (c)(n) is a set.

Therefore, for every n ∈ ω, Wτ (c)(n) is a set.

Proposition 3.4.3. {e | e ∈ Seq(L × C) and e is a τ -orbit of c} is a set.

Proof. By Proposition 3.4.1, for every e ∈ Seq(L × C), if e is a τ -orbit of c, then

–  –  –

is a set.

Proposition 3.4.2 and 3.4.3 will be taken for granted in the sequel.

We write gen τ for a class function from C to Pow Seq(L × C) such that for any c ∈ C,

–  –  –

Assume a class function ε : C → Pow Seq(L × C).

We say that τ generates ε if and only if gen τ = ε.

We say that ε is generable if and only if there is a class function from C to Pow(L × C) that generates ε.

Now, suppose that ε is indeed generable. Can there be more than one class function from C to Pow(L × C) that generates ε?

We could perhaps use the following tentative argument to convince ourselves that this cannot be the case: if τ1 and τ2 are two diﬀerent class functions from C to Pow(L × C), then there must be c ∈ C and l, c ∈ L × C such that either l, c ∈ τ1 (c) and l, c ∈ τ2 (c), or CHAPTER 3. EXECUTION SYSTEMS 69 l, c ∈ τ1 (c) and l, c ∈ τ2 (c); and assuming, without any loss of generality, the former, we can preﬁx any τ1 -orbit of c with l, c to get a τ1 -orbit of c that cannot be a τ2 -orbit of c. But how do we know if there is a τ1 -orbit of c to preﬁx with l, c ?

If τ1 (c ) = ∅, then is a τ1 -orbit of c. If τ1 (c ) = ∅, then we would again expect that there is at least one τ1 -orbit of c. For we could imagine constructing one by ﬁrst choosing a pair l, c in τ1 (c ), then a pair l, c in τ1 (c ), then a pair l, c in τ1 (c ), and so on forever, or until we reach a point where there is no pair to choose. If we never reach such a point, then this construction will involve an inﬁnite number of choices. This suggests that the Axiom of Choice, or some other, weaker form of it, might be necessary to prove the statement that for every suitable τ and c, there is a τ -orbit of c. And indeed, this statement is equivalent to the Axiom of Dependent Choice.

We will need the following lemma:

Lemma 3.4.

4. For every n ∈ ω, if there is l, c ∈ Wτ (c)(n) and e ∈ Seq(L × C) such that e is a τ -orbit of c, then there is e ∈ Seq(L × C) such that e is a τ -orbit of c.

–  –  –

(a) for every class C, every class function τ : C → Pow(L × C), and any c ∈ C, there is e ∈ Seq(L × C) such that e is a τ -orbit of c;

(b) for every non-empty set S and every binary relation R on S, if for every s ∈ S, there is s such that s R s, then there is an inﬁnite sequence d over S such that for every n ∈ ω, head tailn d R head tailn+1 d.

–  –  –

Let s be a member of S.

Since (a) is true, there is e ∈ Seq(L × S) such that e is a τ -orbit of s. And by an easy induction, for every n ∈ ω, tailn e =.

Let d be an inﬁnite sequence over S such that for every n ∈ ω,

–  –  –

Then for every l, c ∈ S, there is l, c such that l, c R l, c, and thus, since (b) is true, there is an inﬁnite sequence d over S such that for every n ∈ ω, head tailn d R head tailn+1 d. And clearly, there is n ∈ ω and l, c ∈ Wτ (c)(n) such that

–  –  –

and tail d is a τ -orbit of c. Thus, by Lemma 3.4.4, there is e ∈ Seq(L × C) such that e is a τ -orbit of c.

Thus, by generalization, (a) is true.

–  –  –

We can now make our tentative argument formal.

Assume class functions τ1, τ2 : C → Pow(L × C).

Proposition 3.4.6. If τ1 = τ2, then gen τ1 = gen τ2.

Proof. Suppose that τ1 = τ2.

Then there is c, l, and c such that either l, c ∈ τ1 (c) and l, c ∈ τ2 (c), or l, c ∈ τ1 (c) and l, c ∈ τ2 (c).

Without any loss of generality, assume the former.

Let e be a sequence in Seq(L × C) that is a τ1 -orbit of c.

·e.

Let e = l, c Then e ∈ (gen τ1 )(c), but e ∈ (gen τ2 )(c). Thus, gen τ1 = gen τ2.

If we think of gen as an operator from cooperations of L-labelled transition coalgebras to cooperations of L-labelled execution coalgebras, then we can read Proposition 3.4.6 as saying that that operator is injective. So it must have a left inverse. The following shows that that left inverse is the composition on the left with the image of the carrier of the

corresponding L-labelled execution coalgebra under η:

Proposition 3.4.7. The following are true:

(a) η(C) ◦ gen τ = τ ;

(b) if ε is generable, then ε = gen(η(C) ◦ ε).

–  –  –

Thus, (b) is true.

Before we move on to our characterization theorem, we have one last stop to make. We have built our notion of generability around the idea of a τ -orbit. And we have tried to formalize the latter in the most conceptually direct way. But as eﬀective as that formalization has been, there is still reason to consider another one. First, it is ugly. And second, there is a very simple but powerful proof rule that it is entirely oblivious to.

We say that ε is consistent with τ if and only if for any c ∈ C and any e ∈ ε(c), one of the

following is true:

–  –  –

(b) there is a class function ε : C → Pow Seq(L × C) such that ε is consistent with τ, and e ∈ ε(c).

Proof. Suppose that (a) is true.

Let ε be a class function from C to Pow Seq(L × C) such that for every c and e, e ∈ ε(c )

if and only if one of the following is true:

–  –  –

Then, by (ii), e ∈ ε(c ). Thus, clause (ii) of the consistency property is true.

Therefore, ε is consistent with τ.

Thus, (b) is true.

Conversely, suppose (b) is true, Then clause (i) of the property of being a τ -orbit of c is true.

By an easy induction, for every n ∈ ω, if tailn e =, then there is l and c such that

–  –  –

Thus, by generalization, clause (ii) of the property of being a τ -orbit of c is true.

Therefore, (a) is true.

The following is immediate:

Corollary 3.4.9. If ε is consistent with τ, then for any c ∈ C,

–  –  –

The following is now straightforward:

Corollary 3.4.10. gen τ is consistent with τ.

Proof. Assume c ∈ C and e ∈ (gen τ )(c).

By Theorem 3.4.8, there is a class function ε : C → Pow Seq(L × C) such that ε is consistent with τ, and e ∈ ε(c).

If τ (c) = ∅ and e =, then there is nothing to prove.

Otherwise, there is l, c, and e such that l, c ∈ τ (c), e ∈ ε(c ), and

–  –  –

And by Corollary 3.4.9, e ∈ (gen τ )(c ).

Thus, by generalization, gen τ is consistent with τ.

Corollary 3.4.9 is the proof rule that we referred to earlier, which is basically an instance of the coinduction proof technique described in [42]. This deserves a brief digression.

We write Gτ (ε) for a class function from C to Pow Seq(L × C) such that for any c ∈ C,

–  –  –

the inclusion class relation on Pow Seq(L × C): for every class function ε1, ε2 : C → Pow Seq(L × C), if for any c ∈ C, ε1 (c) ⊆ ε2 (c), then for any c ∈ C, Gτ (ε1 )(c) ⊆ Gτ (ε2 )(c).

What is more, ε is consistent with τ if and only if ε is a post-ﬁxed point of Gτ, or equivalently, for any c ∈ C, ε(c) ⊆ Gτ (ε)(c).

Pages:     | 1 |   ...   | 6 | 7 || 9 | 10 |   ...   | 12 |

Similar works:

«A META-ANALYSIS OF THE EFFECTS OF INTERVENTIONS TO INCREASE READING FLUENCY AMONG ELEMENTARY SCHOOL STUDENTS By Jiaxiu Yang Dissertation Submitted to the Faculty of the Graduate School of Vanderbilt University in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY in Education and Human Development August, 2006 Nashville, Tennessee Approved: Professor Douglas Fuchs Professor Mark Lipsey Professor Lynn Fuchs Professor Daniel Reschly Professor Donald Compton...»

«Three-dimensional nanofabrication of silver structures in polymer with direct laser writing A dissertation presented by Kevin Lalitchandra Vora to The School of Engineering and Applied Sciences in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the subject of Applied Physics Harvard University Cambridge, Massachusetts February 2014 ©2014 Kevin Lalitchandra Vora All rights reserved. Dissertation advisor: Professor Eric Mazur Kevin Lalitchandra Vora...»

«Perceptions of the Midwife's Role: A Feminist Technoscience Perspective Tracey Cooper, BSc (Hons), Dip (Mid Studies), SM, RM, RGN, EN(G). A Thesis submitted in part fulfilment for the requirements of the Degree of Doctor of Philosophy at the University of Central Lancashire. APRIL 2011. 1 STUDENT DECLARATION I declare that while registered as a candidate for the research degree, I have not been a registered candidate or enrolled student for another ward of the University or other academic or...»

«Thesis word count: 58720 COPYRIGHT STATEMENT This copy of the thesis has been supplied on condition that anyone who consults it is understood to recognise that its copyright rests with its author and that no quotation from the thesis and no information derived from it may be published without the author's prior consent. An Insider Misuse Threat Detection and Prediction Language by Georgios Vasilios Magklaras This dissertation is submitted to the University of Plymouth In fulfilment of the award...»

«Sensationalism, Cinema and the Popular Press in Mexico and Brazil, 1905-1930 By Rielle Edmonds Navitski A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Film and Media in the Graduate Division of the University of California, Berkeley Committee in charge: Professor Kristen Whissel (chair) Professor Natalia Brizuela Professor Mary Ann Doane Professor Mark Sandberg Spring 2013 Sensationalism, Cinema and the Popular Press in Mexico and...»

«TRACKING THE EVOLUTION OF MAGMATIC VOLATILES FROM THE MANTLE TO THE ATMOSPHERE USING INTEGRATIVE GEOCHEMICAL AND GEOPHYSICAL METHODS by Nathalie Vigouroux-Caillibot M.Sc., University of Oregon, 2006 B.Sc., McGill University, 2003 THESIS SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY In the Department of Earth Sciences © Nathalie Vigouroux-Caillibot 2011 SIMON FRASER UNIVERSITY Spring 2011 All rights reserved. However, in accordance with the...»

«SHIFTING PICTURES IN A KALEIDOSCOPIC WORLD: CONCERNS OF PARENTS OF PRESCHOOL CHILDREN WITH DISABILITIES by Susan Wuchenich Parker B.A., The Pennsylvania State University, 1985 M.Ed., The Pennsylvania State University, 1992 Submitted to the Graduate Faculty of the School of Education in partial fulfillment of the requirements for the degree of Doctor of Philosophy University of Pittsburgh 2008 ii UNIVERSITY OF PITTSBURGH SCHOOL OF EDUCATION This dissertation was presented by Susan Wuchenich...»

«THE COLOR OF LOVE ON THE BIG SCREEN: THE PORTRAYAL OF WOMEN IN HOLLYWOOD FILMS IN INTERRACIAL RELATIONSHIPS FROM 1967 TO 2005 By NADIA A. RAMOUTAR 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 Copyright 2006 By Nadia A. Ramoutar To my parents, Chad Ramoutar and Gloria Jean Ramoutar For your courage to love outside the color lines To William, Dorothy, Jean,...»

«THE INFLUENCE OF UNETHICAL PEER BEHAVIOR ON OBSERVERS’ UNETHICAL BEHAVIOR: A SOCIAL COGNITIVE PERSPECTIVE By MICHAEL JAMES O’FALLON A dissertation submitted in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY WASHINGTON STATE UNIVERSITY Department of Management and Operations DECEMBER 2007 To the Faculty of Washington State University: The members of the Committee appointed to examine the dissertation of MICHAEL JAMES O’FALLON find it satisfactory and...»

«ANGLIA POLYTECHNIC UNIVERSITY GENDER RELATIONS, MASCULINITIES AND THE FIRE SERVICE: A QUALITATIVE STUDY OF FIREFIGHTERS’ CONSTRUCTIONS OF MASCULINITY DURING FIREFIGHTING AND IN THEIR SOCIAL RELATIONS OF WORK. DAVE BAIGENT A Thesis in partial fulfilment of the requirements of Anglia Polytechnic University for the degree of Doctor of Philosophy Submitted: May 2001 dave.baigent@fitting-in.com ii ANGLIA POLYTECHNIC UNIVERSITY ABSTRACT SCHOOL OF LANGUAGES AND SOCIAL SCIENCES DOCTOR OF PHILOSOPHY...»

«MENTORING AND PROFESSIONAL IDENTITY DEVELOPMENT FOR AFRICAN AMERICAN FEMALE DOCTORAL STUDENTS: AN EXPLORATORY STUDY By Nettavia Doreen Curry A DISSERTATION Submitted to Michigan State University in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY Higher, Adult and Lifelong Education ABSTRACT MENTORING AND PROFESSIONAL IDENTITY DEVELOPMENT FOR AFRICAN AMERICAN FEMALE DOCTORAL STUDENTS: AN EXPLORATORY STUDY By Nettavia Doreen Curry This dissertation examines the...»

«Intention and the Idea of the Literary in Chaucer by Stephen Andrew Katz A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in English in the Graduate Division of the University of California, Berkeley Committee in charge: Professor Steven Justice, Chair Professor Anne Middleton Professor Niklaus Largier Fall 2009 Intention and the Idea of the Literary in Chaucer © 2009 by Stephen Andrew Katz Abstract Intention and the Idea of the...»

<<  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.