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



Pages:     | 1 |   ...   | 5 | 6 || 8 | 9 |   ...   | 12 |

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

-- [ Page 7 ] --

A plausible remedy for this would, informally, be the following: for any path beginning at a given state, discount any branch off that path that is not a suffix of another path beginning at that same state. And indeed, this would work for this particular case. But there are more problems.

Consider two {l1, l2 }-labelled execution systems, whose executions are as depicted in the

following left and right frames respectively:

CHAPTER 3. EXECUTION SYSTEMS 59

–  –  –

Then s1 and s1 are bisimilar among the two systems. But intuitively, there is difference in branching potential between the two states: the two executions starting from s1 diverge right away at s1, with steps that carry identical labels, whereas those starting from s1 diverge after the first step, at s2, with steps that carry different labels. Of course, the explanation here is that there is no execution starting from s2, and so, conceptually, the choice between the diverging steps is already made at s1. But then, what is the point of having the two executions share the state s2 ?

By now, the reader should begin to suspect what the source of our problems is: what we have called “state” in our systems does not really behave as such. In a type of system that is supposed to serve as a modelling device for processes of some kind, it is essential that “the future behavior depends only upon the current state, and not upon how that state was reached”. And this is not always the case here. What we need to do is constrain the structure of our systems so that it is.

Of course, this idea is not new. The quote above is from [34, p. 176], where Lamport required that the set of paths in a path structure be suffix closed, in the sense that for any path in the set, any suffix of that path is again a path in the set. It was later observed in [20] that this is not enough: one must also require that the set of paths be fusion closed, in the sense that for any prefix of a path in the set, and any suffix of another path in the set, if the former ends at the state at which the latter begins, then their fusion at that state is again a path in the set (see [52]). And apparently, it was Abrahamson, in [1], that first considered path structures that satisfied both requirements (see [16]).

We now adapt these requirements to our own setting.

We say that S, E is Abrahamson if and only if the following are true:

–  –  –

In an Abrahamson system, there is a clear notion of a “possible next step” relation, which induces the construction of an associated, or better, underlying labelled transition system.

From a mathematical standpoint, this construction makes sense for a non-Abrahamson system as well, and is most conveniently carried out on the coalgebra side of the theory.

Assume a class C.

We write η(C) for a class function from Pow Seq(L × C) to Pow(L × C) such that for every S ∈ Pow Seq(L × C),

–  –  –

Our choice of notation here is not arbitrary. We think of η as an operator that assigns to every class C a class function from its image under Pow ◦ Seq ◦ (L × Id) to its image under Pow ◦ (L × Id). And what is interesting about this operator is that for every class function f : C1 → C2,

–  –  –

In the language of category theory, this makes η a natural transformation from Pow ◦ Seq ◦ (L × Id) to Pow ◦ (L × Id).

The concept of natural transformation is of great importance in the study and application of category theory. It is defined using the same property as above, only generalized to a pair of arbitrary functors with a common domain category and a common codomain one. Pierce helps us visualize the essence of the concept by inviting us to “imagine ‘sliding’ the picture defined by [the first functor] onto the picture defined by [the second one]” (see [47, p. 41]).

The reason why it is of interest to us here that η is a natural transformation is a theorem by Rutten, according to which, every natural transformation ν from an endofunctor F1 on Class to an endofunctor F2 on Class induces a functor from F1 -Coalg to F2 -Coalg that assigns to every F1 -coalgebra C, γ the F2 -coalgebra C, η(C) ◦ γ, and to every homomorphism h from an F1 -coalgebra C1, γ1 to an F1 -coalgebra C2, γ2 that same class CHAPTER 3. EXECUTION SYSTEMS 61 function h, which is now a homomorphism from the F2 -coalgebra C1, η(C1 ) ◦ γ1 to the F2 -coalgebra C2, η(C2 ) ◦ γ2 (see [56, thm. 15.1]). In other words, the induced functor preserves homomorphisms, and thus, by Theorem 2.2.10, bisimulations too.

In our case, the functor induced by η is a forgetful functor, which, informally, keeps only the first step, if any, from any execution starting from any state, and discards the rest.

The following is immediate from Rutten’s theorem, but a more direct proof would require

only little extra work:

Proposition 3.3.1. If h is a homomorphism from C1, ε1 to C2, ε2, then h is a homomorphism from the L-labelled transition coalgebra C1, η(C1 ) ◦ ε1 to the L-labelled transition coalgebra C2, η(C2 ) ◦ ε2.

The following is now immediate from Theorem 2.2.10 and Proposition 3.3.1.





Proposition 3.3.2. If B is a bisimulation between C1, ε1 and C2, ε2, then B is a bisimulation between the L-labelled transition coalgebras C1, η(C1 ) ◦ ε1 and C2, η(C2 ) ◦ ε2.

Of course, we can translate all this back to the system side of the theory.

Assume a binary relation E : S ↔ S (L × S).

We write trans E for a binary relation between S and L × S such that for any s ∈ S and any l, s ∈ L × S,

–  –  –

The following is trivial:

Proposition 3.3.3. trans E = rel(η(S) ◦ fun E).

The following is now immediate from Proposition 2.2.1(b), 2.2.15, 3.2.4, 3.3.2, and 3.3.3:

Proposition 3.3.4. If B is a bisimulation between S1, E1 and S2, E2, then B is a bisimulation between the L-labelled transition systems S1, trans E1 and S2, trans E2.

–  –  –

First, suppose that S, E and S, E are two {l}-labelled execution systems, whose

executions are as depicted in the following left and right frames respectively:

–  –  –

Then s1 and s1 are bisimilar among the {l}-labelled transition systems S, trans E and S, trans E, but not among S, E and S, E.

The problem is easy to spot here. The two systems have one execution each. But whereas the execution of the first system has only one step, the execution of the second has two.

And that second step, which is the cause for s1 and s1 not being bisimilar among the two systems, is dropped during the labelled transition system construction.

Now suppose that S, E and S, E are two {l1, l2, l3 }-labelled execution systems, whose

executions are as depicted in the following left and right frames respectively:

–  –  –

Then s1 and s1 are bisimilar among the now {l1, l2, l2 }-labelled transition systems S, trans E and S, trans E, but not among S, E and S, E.

Here the problem is of a different nature. Every step of every execution is accounted for in the constructed labelled transition systems. However, the two longer executions, starting from s1 and s1 respectively, disagree on their second step, and that disagreement is masked by the agreement of executions starting from s2 and s2 respectively.

These two examples were specially chosen to target the two defining clauses of the Abrahamson property. Specifically, and informally, the systems in the first example are not suffix closed, thus violating clause (i) of the property, whereas those in the second are not CHAPTER 3. EXECUTION SYSTEMS 63 fusion closed, thus violating clause (ii). Overall, none of them is Abrahamson. And since our construction was based on the idea of a “possible next step” relation, which, in the case of a non-Abrahamson system, is a conceptually ambiguous notion, it is no surprise that non-bisimilar states turn bisimilar in the constructed systems.

With Abrahamson systems, things get much more interesting. In the rest of our examples, we shall focus on such systems. And as afforded with such systems, we shall communicate their structure more casually, simply drawing a diagram of the underlying labelled transition system, and describing the set of paths in that diagram that correspond to their executions.

Consider then the {l1, l2 }-labelled transition system, with l1 and l2 different, portrayed in

the following diagram:

s l1 l2

One {l1, l2 }-labelled execution system lying over this labelled transition system is the one whose executions correspond to all infinite paths in the diagram. Another is the one whose executions correspond to those infinite paths that go through each of the two loops infinitely often. And of course, s is not bisimilar with itself among the two.

We may think of each of the two {l1, l2 }-labelled execution systems in this example as a specification of a scheduling policy between two processes, forever iterating over l1 and l2 respectively, on a single processing unit. Under the first policy, the scheduler is only required to guarantee progress of execution, simply picking at random one process at a time. Under the second, it is further required to be fair, taking care that there is no point in time after which a process is forever neglected. But whereas its behaviour in the first case is completely specified by the underlying {l1, l2 }-labelled transition system, in the second case, it cannot be specified by any {l1, l2 }-labelled transition system alone.

Besides demonstrating the failure of the converse of Proposition 3.3.4 for Abrahamson systems, this example attempts to display the increase in expressive power and branching complexity that moving from a labelled transition to a labelled execution system can bring.

But it does so inadequately. For one need not really move to a labelled execution system to specify the behaviour of the scheduler under that second policy. One can just augment the given labelled transition system with the set of all infinite sequences over {l1, l2 } corresponding to a fair interleaving of the two processes. And in fact, the concept of bisimulation between labelled transition systems can be generalized to account for this kind of augmentation by simply adding a third clause to Definition 2.1.3 that tests for inclusion between the sets of “admissible” sequences of labels associated with each state. This gives rise to the less known concept of fortification equivalence, one of the alternative approaches to the semantics of finite delay considered by Milner in [38], and a perfectly adequate CHAPTER 3. EXECUTION SYSTEMS 64 approach to the specification of the two scheduling policies in our example. What we want is another example that will expose the shortcomings of this type of approach, and vindicate our present venture.

Consider then the {l1, l2 }-labelled transition system, with l1 and l2 different, portrayed in

the following diagram:

–  –  –

The first {l1, l2 }-labelled execution system that we wish to consider here is the unique Abrahamson system whose executions starting from s1 correspond to all maximal paths in this diagram. The second is the one whose executions are all the executions of the first, except the single infinite execution stuttering around s1. And because of this exception, s1 is not bisimilar with itself among the two systems.

This beautiful example is from [4], where it was used to attack precisely the type of approach discussed above. Here, it is perhaps convenient to think of the two systems as modelling the behaviour of two distinct processes, both initialized at s1. The first process will either loop around s1 forever, or iterate through it for a finite, indeterminate number of times before progressing to s2. From there on, a single indeterminate choice will decide its fate. The second process, on the other hand, is not allowed to loop around s1 forever. It must eventually advance to s2, from where on it behaves just like the first one. What sets the behaviour of the two processes apart is, of course, the infinite stuttering around s1, permitted for the first process, but not the second. However, this is something that cannot be determined by the sequences of actions that the two processes perform in the course of their executions, for the trace of that infinite stuttering is matched by that of every infinite execution that eventually loops around s2. And yet the two processes ought to be distinguished. For during that infinite stuttering, the first process may always choose to branch off to a state from which it can perform l2, whereas, in every execution having that trace, the second must eventually reach a state from which it cannot ever do so.

With respect to the failure of the converse of Proposition 3.3.4, both this and the previous example point at the same problem: the existence of an infinite path in the diagram that does not correspond to any execution of a system, but whose every finite prefix is a prefix of another path that does.

CHAPTER 3. EXECUTION SYSTEMS 65 This too is something that has already come up in the investigation of path structures in temporal logic.



Pages:     | 1 |   ...   | 5 | 6 || 8 | 9 |   ...   | 12 |


Similar works:

«INFORMATION IN FINANCIAL MARKETS by Bin Chang A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Graduate Department of Joseph L. Rotman School of Management University of Toronto ©Copyright by Bin Chang, 2008 Abstract Information in Financial Markets by Bin Chang Doctor of Philosophy Joseph L. Rotman School of Management University of Toronto 2008 This thesis studies information in financial markets from three perspectives: the role of information...»

«Rick Grush Introduction to emulation 1 An introduction to the main principles of emulation: motor control, imagery, and perception Rick Grush Department of Philosophy 0119 rick@mind.ucsd.edu UC San Diego http://mind.ucsd.edu 9500 Gilman Drive La Jolla, CA 92093-0119 0. Introduction 1. Motor control: forward models and Kalman filters 1.1 Feed-forward and feedback control 1.2 Emulators (forward models) 1.3 Kalman filters 1.4 Kalman filtering and control 1.5 Motor control 2. Motor Imagery 2.1 The...»

«INPUT-POWERED INTERFACE CIRCUITS FOR ELECTRODYNAMIC VIBRATIONAL ENERGY HARVESTING SYSTEMS By YUAN RAO 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 1 © 2013 Yuan Rao 2 To the memory of my father 3 ACKNOWLEDGMENTS This work was funded in part by Texas Instruments® through a fellowship. My most heartfelt thanks go to my advisor, Dr. David P. Arnold, for his...»

«AN APOSTOLIC APPROACH FOR THE EVANGELIZATION OF POSTMODERN PEOPLE _ A Dissertation Presented to the Faculty of the School of Theology Southwestern Baptist Theological Seminary Fort Worth, Texas _ In Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy _ Department of Evangelism _ by Eric J. Thomas May 2002 ©Copyright by Eric J. Thomas 2002 All Rights Reserved INTRODUCTION Jesus Christ established the mission of the church through His command in Acts 1:8. This command to...»

«UNIVERSITY OF CALGARY Selected Poems of Sandro Penna by Aaron Giovannone A THESIS SUBMITTED TO THE FACULTY OF GRADUATE STUDIES IN PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY DEPARTMENT OF ENGLISH CALGARY, ALBERTA JANUARY 2014 © Aaron Giovannone 2014 Abstract This dissertation is a selection and translation of the poetry of Sandro Penna (1906 Perugia – 1977 Rome), an important figure in Italian twentieth-century literature who remains largely unknown to...»

«Science and technology in Medieval Islam What is Islam? Islam is a religion that began in the 7th century with the prophet Muhammad in Mecca. Muhammad believed that he was a messenger sent by God to teach people the right way to live. ‘Islam’ is an Arabic word which means ‘submission to God’. The holy book of Islam is the Qur’an (‘Koran’), and the centre for Muslim worship is the ‘House of Prayer’ in Mecca. During the 6th century, Arabia had two powerful neighbours: the...»

«FACTORS INFLUENCING RESIDENTS'ATTITUDE TOWARDS TOURISM DEVELOPMENT ON THE REMOTE ISLAND OF SOCOTRA, YEMEN HUSSEIN ABDULQADER AL-GAHURI DOCTOR OF PHILOSOPHY LINIVERSITI UTARA MALAYSIA JULY 2014 FACTORS INFLUENCING RESIDENTS'ATTITUDE TOWARDS TOURISM DEVELOPMENT ON THE REMOTE ISLAND OF SOCOTRA, YEMEN BY HUSSEIN ABDULQADER AL-GAHURI Thesis Submitted to Ghazali Shafie Graduate School of Govrnment, Universiti Utara Malaysia, in Fl~lfillment the Requirement for the Degree of Doctor of Philosophy of...»

«Queering Home: Domestic Space and Sexuality in Postmodern American Literature by Jason Bryant A Dissertation Presented in Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy Approved November 2013 by the Graduate Supervisory Committee: Deborah Clarke, Chair Robert Sturges Lee Bebout ARIZONA STATE UNIVERSITY December 2013 ABSTRACT This dissertation explores narratives of homosexuals and trans men and women occupying domestic spaces, discerning the ways that “home”...»

«The Juggler in Shakespeare: Con-Artistry, Illusionism, and Popular Magic in Three Plays August 2010 J.A. Shea Department of English McGill University, Montréal A thesis submitted to McGill University in partial fulfilment of the requirements of the degree of Doctor of Philosophy i Abstract This dissertation argues that Shakespeare’s plays Othello, The Taming of the Shrew, and The Winter’s Tale engage deeply with representations of, and associations with, that early modern social person...»

«The Dark Side of European Integration: Nationalism and Radical Right Mobilization in Contemporary Europe By Alina Naumovna Polyakova A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Sociology in the Graduate Division of the University of California, Berkeley Committee in charge: Neil Fligstein, Chair Dylan Riley Jason Wittenberg Fall 2013 The Dark Side of European Integration: Nationalism and Radical Right Mobilization in...»

«Trickster Skins: Narratives of Landscape, Representation, and the Miami Nation A DISSERTATION SUBMITTED TO THE FACULTY OF THE GRADUATE SCHOOL OF THE UNIVERSITY OF MINNESOTA BY Scott Michael Shoemaker IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Dr. Brenda Child, Adviser July 2011 © Scott M. Shoemaker, 2011 Acknowledgements I owe a tremendous amount of gratitude and appreciation to numerous people in my success in graduate school. The American Studies and...»

«YET ANOTHER ANTI-MOLINIST ARGUMENT∗ Dean Zimmerman Rutgers University I. Motivating Molinism Introduction “Molinism”, in contemporary usage, is the name for a theory about the workings of divine providence. Its defenders include some of the most prominent contemporary Protestant and Catholic philosophical theologians.1 Molinism is often said to be the only way to steer a middle course between two extremes: the radically opposed conceptions of foreknowledge, providence, and grace...»





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