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



Pages:   || 2 | 3 | 4 | 5 |   ...   | 12 |

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

-- [ Page 1 ] --

Axioms for Asynchronous Processes

by

Eleftherios Matsikoudis

A dissertation submitted in partial satisfaction of the

requirements for the degree of

Doctor of Philosophy

in

Electrical Engineering and Computer Sciences

in the

Graduate Division

of the

University of California, Berkeley

Committee in charge:

Professor Edward A. Lee, Chair

Professor Christos H. Papadimitriou

Professor Leo A. Harrington

Fall 2010

Axioms for Asynchronous Processes

Copyright 2010 by Eleftherios Matsikoudis Abstract Axioms for Asynchronous Processes by Eleftherios Matsikoudis Doctor of Philosophy in Electrical Engineering and Computer Sciences University of California, Berkeley Professor Edward A. Lee, Chair From classical computability theory to modern programming language design, the mathematical concept of function has dominated our perception of sequential computation.

But as soon as we venture into the realm of concurrent interaction, it is well understood that this concept has to be abandoned. What are we to replace it with?

This question is considered too general to admit a definitive answer. If we want such an answer, we must be willing to narrow our scope, and impose some constraint on the form of concurrent interaction that we choose to consider. Here, we derive such a constraint solely from the intuitive notion of asynchrony. And under this constraint, we propose a mathematical concept of sequential asynchronous process, which we define axiomatically, and put forward as the sought replacement to the classical function.

Our theory is an interleaving theory. And traditionally, interleaving theories have failed to integrate a satisfactory treatment of what is known as the finite delay property, according to which, if a process can make progress, then it will eventually do so, but after an arbitrary amount of time. This failure is generally attributed to the so-called expansion law of such theories, which reduces parallel execution to indeterminate serialization. But in truth, the problem is deeply rooted in the concept of labelled transition system, which is the pervasive mathematical object underlying such theories.

To solve this problem, we introduce a new type of system, in which, instead of labelled transitions, we have, essentially, sequences of labelled transitions. We call systems of this type labelled execution systems. We use a coalgebraic representation to obtain a proper concept of bisimilarity among such systems, and study the conditions under which that concept agrees with the intuitive notion of branching equivalence that one has for them.

Finally, we examine the difference in expressive power and branching complexity between labelled execution systems and labelled transition systems.

The intended interpretation of our concept of asynchronous process is a state of what we

–  –  –

Chapter 1 Introduction From classical computability theory to modern programming language design, the mathematical concept of function has dominated our perception of sequential computation.

But as soon as we venture into the realm of concurrent interaction, it is well understood that this concept has to be abandoned. What are we to replace it with?

This question is considered too general to admit a definitive answer. If we want such an answer, we must be willing to narrow our scope, and impose some constraint on the form of concurrent interaction that we choose to consider. Here, we derive such a constraint solely from the intuitive notion of asynchrony. And under this constraint, we propose a mathematical concept of sequential asynchronous process, which we define axiomatically, and put forward as the sought replacement to the classical function.

Our theory is an interleaving theory. And traditionally, interleaving theories have failed to integrate a satisfactory treatment of what is known as the finite delay property, according to which, if a process can make progress, then it will eventually do so, but after an arbitrary amount of time. This failure is generally attributed to the so-called expansion law of such theories, which reduces parallel execution to indeterminate serialization. But in truth, the problem is deeply rooted in the concept of labelled transition system, which is the pervasive mathematical object underlying such theories.

To solve this problem, we introduce a new type of system, in which, instead of labelled transitions, we have, essentially, sequences of labelled transitions. We call systems of this type labelled execution systems. We use a coalgebraic representation to obtain a proper concept of bisimilarity among such systems, and study the conditions under which that concept agrees with the intuitive notion of branching equivalence that one has for them.

Finally, we examine the difference in expressive power and branching complexity between labelled execution systems and labelled transition systems.

The intended interpretation of our concept of asynchronous process is a state of what we

CHAPTER 1. INTRODUCTION 2

may think of as a very large labelled execution system, and the role of our axioms is to fix the shape of that system.

There are two groups of axioms. The first group is used to specify the form of the executions of the system, and the way in which they branch off one another, in a manner consistent with our intuitive notion of behaviour of an asynchronous process. The second group is deduced from a single extremal axiom asserting the finality of the system in a covariety of coalgebras relating to the first group of axioms, and is used to guarantee that every behaviour is accounted for exactly once.





Chapter 2 Transition Systems

2.1 Basic definitions Definition 2.1.1. A transition system is an ordered pair S, T such that the following are

true:

–  –  –

(b) T is a binary relation1 on S.

Assume a transition system S, T.

We write s −→T s if and only if s T s.

We call any s ∈ S a state of S, T, and any s, s ∈ graph T a transition of S, T.

The concept of transition system is ubiquitous in computer science: Turing machines, rewriting systems, Kripke structures are only but a few examples. But as versatile as it is, one cannot use it to model anything more about an individual transition than a change of state in the system. And we will need more than that.

Assume a non-empty set L of labels.

–  –  –

(b) T is a binary relation between S and L × S.

Assume an L-labelled transition system S, T.

l We write s −→T s if and only if s T l, s.

We call any s ∈ S a state of S, T, and any s, l, s ∈ graph T a transition of S, T.

Labelled transition systems have been around at least since Moore’s work on finite automata in [43], where they appeared in tabular as well as pictorial form. In their present form, they were first introduced by Keller in [32], where they were called named transition systems. And although Keller used them to model parallel computation, it was apparently Milner who first saw labels as shared vehicles of interaction, and labelled transition systems as models of communicating behaviour, paving the way for [37] and the advent of process algebra.

Assume L-labelled transition systems S1, T1 and S2, T2.

Definition 2.1.3. A bisimulation between S1, T1 and S2, T2 is a binary relation

B : S1 ↔ S2 such that for any s1 and s2 such that s1 B s2, the following are true:

–  –  –

s0 and s0 are bisimilar among the first two diagrams; neither of them is bisimilar to s0.

The idea of bisimilarity is that for any path branching out of either one of the two states, there is a path branching out of the other one, that carries the same labels in the same order, and goes through states that are again related to the corresponding states of the first path in the same way. This last piece of recursion is what separates bisimilarity from trace equivalence, making the former sensitive to the branching potential of each state.

Notice that a transition system can be thought of as a labelled transition system, every transition of which is decorated with a single fixed label. This induces a concept of bisimulation between transition systems: simply erase every instance of l in the above definition.2 The concept of bisimulation is due to David Park (see [46]), and is without doubt the most significant contribution of the theory of concurrency to the broader arena of computer science and mathematics at large.3 After learning about Milner’s work in [39], where bisimulation was worked out in the context of a calculus for the first time, and prompted by the perception of an analogy between the mathematical notion of a set and that of a process with just one kind of action, Peter Aczel used transition systems to model a theory of sets that need not be well founded, and the concept of bisimulation to strengthen, in a sensible and pleasing way, the Axiom of Extensionality therein (see [2]).4 But then he went further. He noticed that transition systems could be viewed as coalgebras for a certain endofunctor, and models of his axiom as final objects in a suitable category of such coalgebras. Work on a generalization of this result culminated in [5] to bear a final coalgebra theorem, asserting the existence of final coalgebras for a wide range of common endofunctors, and a categorical definition of bisimulation, generalizing the latter as a viable This will be a common theme throughout this and the next chapter: we will often state definitions and prove statements only for the labelled case; a proper “unlabelling” will immediately carry these over to the non-labelled case.

To be fair, the concept of bisimulation has been independently discovered in the fields of modal logic and set theory as well. See [58] for a comprehensive historical account.

Forti and Honsell had already discovered and used the concept of bisimulation to that end in [22]. But here, we are not so much interested in non-well-founded set theory, but rather in the developments following Aczel’s work on it.

CHAPTER 2. TRANSITION SYSTEMS 6 coalgebraic dual to the algebraic notion of congruence.

This led eventually to a general theory of universal coalgebra (see [56]).

We will now begin to recast things in this coalgebraic framework. This will be of great technical as well as conceptual use, especially in the next chapter, when we replace the concept of transition system with another one, more apt to our purpose. Working with coalgebras, we will need to make reference to a few common concepts from category theory, and some familiarity with the latter will at times be useful. But such familiarity is not assumed, and we will make an effort to supplement each category-theoretic definition or argument with a concrete explanation.

2.2 From systems to coalgebras Consider once more the concept of transition system. We have formalized this as a set of states together with a binary relation on that set. But there is another way: to look at this binary relation as a set-valued function.

Assume sets S1 and S2.

Assume a binary relation R : S1 ↔ S2.

We write fun R for a function5 from S1 to P S2 such that for any s1 ∈ S1,

–  –  –

By Proposition 2.2.1, a transition system S, T can be represented as a function from S to P S, namely as fun T, and conversely, a function τ : S → P S can be represented as a transition system, namely as S, rel τ. Thus, we could alternatively define a transition system to be a function from a set to the power set of that set, or more verbosely, a pair of a set S and a function τ : S → P S. This would be a coalgebraic definition, one we shall have more to say about after a more general introduction into the concept of coalgebra.

A coalgebra is defined relative to an endofunctor, and an endofunctor is defined relative to a category.

A category is just a two-sorted partial algebra of objects and arrows, with an identity, a domain, a codomain, and a composition operation, satisfying a couple of simple equational axioms. These operations assume their suggested meaning in every concrete category, where any object is a set, possibly with some structure, and any arrow is a function from one set to another, typically preserving structure.

For reasons that will soon become clear, we shall want to work with some very large categories, the collections of whose objects and arrows are not sets, not even proper classes.

The first such category that we will be working with is the category of all classes7 and all class functions8 between them.

We write Class for the category whose objects are all the classes, and arrows all the class functions.

It is of course only in a generalized sense that we may think of Class as a partial algebra.

All the same, we shall not worry too much about this, or any other issue of foundational nature. Such issues can be addressed in one way or another (for example, see [35, chap. I] or [6, chap. 2]), but a thorough treatment here would only obscure the presentation of our ideas. And in any case, we will avoid impredicative constructions and comprehension principles that test the consistency of the theory.

A functor is a category homomorphism: a structure-preserving map from one category to another.

An endofunctor is a functor from a category to that same category.

For example, an endofunctor on Class is a map from Class to Class that maps classes to classes and class functions to class functions, preserving the identity operation on classes, and the domain, codomain, and composition operation on class functions.

A collection C of sets is a class if and only if there is a unary formula ϕ of set theory such that for every set S, S ∈ C if and only if ϕ(S) is true.

A class function f is an ordered triple D, C, G such that D is a class, C is a class, G ⊆ D × C, and for every d, c1 and c2, if d, c1 ∈ G and d, c2 ∈ G, then c1 = c2. We write dom f for D, cod f for C, and graph f for G. We call dom f the domain of f, cod f the codomain of f, and graph f the graph of f.



Pages:   || 2 | 3 | 4 | 5 |   ...   | 12 |


Similar works:

«ZEKI SARITOPRAK, PH.D. Department of Theology and Religious Studies John Carroll University University Heights, OH 44118 (216)397-4935 zsaritoprak@jcu.edu EDUCATION THE UNIVERSITY OF MARMARA, Istanbul, Turkey Ph.D. in Islamic Theology, Institute of Social Sciences, 1991 Dissertation: The Antichrist (al-Dajjal) in Islamic Theology Examines the concept of al-Dajjal in the main sources of Islam, in particular the Qur’an, the Hadith, and their exegeses. Includes specific analysis of...»

«A RICH METADATA FILESYSTEM FOR SCIENTIFIC DATA A Dissertation Submitted to the Graduate School of the University of Notre Dame in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy by Hoang Bui, Dr. Douglas Thain, Director Graduate Program in Computer Science and Engineering Notre Dame, Indiana May 2012 A RICH METADATA FILESYSTEM FOR SCIENTIFIC DATA Abstract by Hoang Bui As scientific research becomes more data intensive, there is an increasing need for scalable,...»

«Neural dynamics in cortical populations Marius Pachitariu Dissertation submitted for the degree of Doctor of Philosophy of University College London Gatsby Computational Neuroscience Unit University College London 2014 Declaration I, Marius Pachitariu, declare that this thesis was composed by myself, that the work contained herein is my own except where explicitly stated otherwise in the text, and that this work has not been submitted for any other degree or professional qualification except...»

«MARK SCROGGINS Curriculum Vitae 561.218.8769 (fax) • mscroggi@fau.edu Associate Professor, Department of English Florida Atlantic University 777 Glades Road Boca Raton, Florida 33431 EDUCATION CORNELL UNIVERSITY Ph.D. in English, 1993 Dissertation: “Zukofsky and Stevens: Poetry, Music, and Knowledge” M.A. in English, 1990 M.F.A. in English (poetry writing), 1990 VIRGINIA POLYTECHNIC INSTITUTE AND STATE UNIVERSITY B.A. in English (in honors) and Philosophy, Magna Cum Laude, 1986...»

«ˆ NOUS 46:4 (2012) 675–708 Contrastive Knowledge Surveyed JONATHAN SCHAFFER Australian National University JOSHUA KNOBE Yale University Suppose that Ann says, “Keith knows that the bank will be open tomorrow.” Her audience may well agree. Her knowledge ascription may seem true. But now suppose that Ben—in a different context—also says “Keith knows that the bank will be open tomorrow.” His audience may well disagree. His knowledge ascription may seem false. Indeed, a number of...»

«“In soft Complaints no longer Ease I find”: Poetic Configurations of Melancholy by Early Eighteenth-Century Women Poets. DISSERTATION zur Erlangung des akademischen Grades doctor philosophiae (Dr. phil.) eingereicht an der Philosophischen Fakultät II der Humboldt-Universität zu Berlin und erfolgreich verteidigt am 31.10.2013 von Sabine Blackmore Präsident der Humboldt-Universität zu Berlin: Prof. Dr. Jan-Hendrik Olbertz Dekanin der Philosophischen Fakultät II: Prof. Dr. Helga Schwalm...»

«WEED MANAGEMENT PLAN Asotin County Noxious Weed Control Board P.O. Box 881 Asotin, WA 99402 (509) 243-2098 Table of Contents I General Information Page Introduction 3 Asotin County Noxious Weed Control Board 3 Weed Board Philosophy 4 Goal 4 Mission Statement 4 Local Land Management Agencies 5 Services, Materials and Information 5 Board Meetings 5 Weed Control Districts 6 District Map 7 Ongoing Projects 8,9 II Noxious Weeds Page Bull thistle (Cirsium vulgare) 11 Canada thistle (Cirsium arvense)...»

«SCOPE PARALLELISM AND THE RESOLUTION OF ELLIPSIS AT THE SYNTAX/SEMANTICS INTERFACE Gun ERRE ZREXACH JAVIER In this paper several scope asymmetries in VP ellipsis constructions in English and Spanish are studied. It is argued that an approach based on Fox' (1995 a,b) Ellipsis Scope Generalization faces numerous conceptual and empirical problems. Ellipsis resolution is conceived of as a phenomenon belonging to the conceptual-intentional pan of the computational system that is conditioned by the...»

«UCGE Reports Number 20185 Department of Geomatics Engineering An Analysis on the Optimal Combination of Geoid, Orthometric and Ellipsoidal Height Data (URL: http://www.geomatics.ucalgary.ca/links/GradTheses.html) by Georgia Fotopoulos December 2003 UNIVERSITY OF CALGARY An analysis on the optimal combination of geoid, orthometric and ellipsoidal height data by Georgia Fotopoulos A THESIS SUBMITTED TO THE FACULTY OF GRADUATE STUDIES IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF...»

«Gods Who Hear Prayers: Popular Piety or Kingship in Three Theban Monuments of New Kingdom Egypt. By Cindy Lee Ausec A dissertation submitted in partial satisfaction of the requirements for the degree of Joint Doctor of Philosophy with Graduate Theological Union in Near Eastern Religions in the Graduate Division of the University of California, Berkeley Committee in Charge: Professor Carol Redmount, Chair Professor Marian Feldman Professor Aaron Brody Professor Robert B. Coote Professor Anthony...»

«Mandibular Growth in Australopithecus robustus by Zachary Daniel Cofran A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Anthropology) in the University of Michigan Doctoral Committee Professor, Milford H. Wolpoff, Chair Professor, Laura M. MacLatchy Assistant Professor, Eric A. Hetland Assistant Professor, Adam P. Van Arsdale, Wellesley College © Zachary Cofran All rights reserved Acknowledgements There is absolutely no way I could...»

«A study on the control of NOx and Particulate Matter emissions from Dimethyl Ether combustion in compression ignition engines George Thomas B.Tech, M.E, M.Phil (Mechanical Engineering) A thesis submitted for the degree of Doctor of Philosophy at The University of Queensland in 2015 School of Mechanical and Mining Engineering i Abstract Dimethyl Ether (DME) is a new age fuel developed mainly from coal and natural gas to use in compression ignition (CI) engines relatively easily with minimum...»





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