FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 4 | 5 || 7 | 8 |   ...   | 12 |

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

-- [ Page 6 ] --

Here, we will feel comfortable working with large coalgebras, and refrain from imposing additional constraints, just for the sake of size. Indeed, the very reason that we have decided to work within a theory of classes in the first place was not having to worry about size at all. If we want to understand ‘behaviour’ in terms of branching structure, then it seems inappropriate to constrain that structure by means that only reflect our own CHAPTER 2. TRANSITION SYSTEMS 49 preconceptions about how that ‘behaviour’ may come about. And a bound on the branching degree of that structure seems to do just that: reflect our own bias toward a kind of process that “computes” its own evolution using a fixed set of predefined resources.

Before we leave this chapter, we note that the notion of an F -coalgebra can be defined for any endofunctor F on any arbitrary category, concrete or not. See, for example, [57], for an adaptation of the theory to the categories of metric spaces and ordered sets, or [51], for an entirely axiomatic approach.

Chapter 3 Execution Systems

3.1 From transitions to executions Perhaps the first thing to decide when setting out to develop an observational theory of processes of some kind is what the unit of observation should be. For a theory based on the concept of labelled transition system, this unit is effectively fixed to what can be represented by a single transition: a single action or event. But at that scale of observation, it is only the local properties of the behaviour of a process that carry over to the model. Non-local properties, specifically those concerning infinite executions of the process, do not. For examples of the first kind, one may look at safety properties, such as mutual exclusion or deadlock freedom, whereas for examples of the second kind, one may look at liveness properties, such as termination or guaranteed service (see [8]).

We might think of a labelled transition system as an intuitionistic approach to a model of a process. For an intuitionist, an infinite execution cannot possibly claim existence as a completed totality of actions or events. It is only “a manifold of possibilities open towards infinity; it remains forever in the status of creation, but is not a closed realm of things existing in themselves” (see [63, p. 9]). This rejection of the notion of actual infinity is detrimental to the expressiveness of a theory. All limits of partial executions become complete executions in the model, which is the source of bounded indeterminacy (see [19, chap. 9]), and the reason behind the well known problems with properties like fairness ([50]) or finite delay ([30]) (for example, see [45]).

Here, instead, we take what we might say is a more classical approach, and fix our unit of observation at the level of a complete execution of a process. And for that, we need a different type of mathematical structure.

–  –  –

We call any s ∈ S a state of S, E, and any s, e ∈ graph E an execution of S, E.

Notice that an execution is an ordered pair of a state and a sequence of states, rather than a single sequence of states, what might have seemed a more natural option. And while we do think that there is a certain clarity in distinguishing the starting state of an execution from any subsequent step, this was mainly a choice of mathematical convenience. Its merit will soon become apparent.

The idea of an execution system has been around at least since the early days of temporal logic in computer science, in the form of a type of semantic structure called a path structure in [53] (for example, see [52], [1], and [34]). The states of a system would represent the various memory configurations and control locations traversed in the course of a computation of a possibly concurrent program, and the executions those computations permitted by the assumed implementation, and over which the modalities of the logic were to be interpreted. Here, we will need one more thing: labels.

Definition 3.1.2. An L-labelled execution system is an ordered pair S, E such that the

following are true:

–  –  –

We call any s ∈ S a state of S, E, and any s, e ∈ graph T an execution of S, E.

Despite the rich cross-fertilization of ideas between temporal logic and process algebra, and the obvious parallel between semantic structures and labelled systems in the two fields, path structures were never really assimilated for use as models of process theories. In fact, the concept of labelled execution system is almost absent from the literature. Looking back For every set S, we write S S for the set of all finite and infinite sequences over S.

CHAPTER 3. EXECUTION SYSTEMS 52 to it, we could only find a handful of sporadic instances of the general notion.

We discuss them at the end of this chapter, where we also offer our own opinion on this surprising omission.

3.2 From systems to coalgebras and back As our choice of formalization should have made obvious, the concept of labelled execution system is a direct generalization of that of labelled transition system. The idea of a single step from one state to another is replaced by that of an “admissible” path through the system over which a sequence of steps can be taken. The result is a more elaborate notion of branching structure. And if we are to associate this notion with ‘behaviour’ of some kind, we need to understand what constitutes similarity and dissimilarity of it. In other words, we need a concept of branching equivalence suited to labelled execution systems.

What should that concept be?

In [57], Rutten and Turi propose a simple approach to this type of problem: all we have to do is find a suitable endofunctor to represent our systems coalgebraically. We can then use that endofunctor to instantiate the “parametric” concept of bisimulation of Definition 2.2.8, and obtain not only the equivalence concept that we seek, but a model too that is fully


with respect to that concept (see Theorem 2.4.13 and 2.5.1).2 This is straightforward here.

We write Seq for an endofunctor on Class that assigns to every class C the class

–  –  –

At this point, the reader may protest against the seeming circularity in the way we have specified the action of Seq on class functions; what may look like a harmless definition by recursion is really a descending argument over a possibly infinite deduction sequence: there is no base case. A little thought, however, will suffice to convince oneself that there is nothing ambiguous about it. Seq f is a simple lift of f to sequences over dom f. Informally, if c0, c1,... is a sequence over dom f, then (Seq f )( c0, c1,... ) is the result of replacing each ci in that sequence with its own image under f, namely the sequence f (c0 ), f (c1 ),.... We are thus entitled to use this contentious form of specification as a definition. The question is how do we justify it formally.

In principle, we could use induction on the index of a sequence to prove that each point in the sequence is uniquely determined. But we can do better.

First, notice that Seq C2 can be given the structure of a ({ } + (C2 × Id))-coalgebra, where { } + (C2 × Id) is the composite of the left sum endofunctor { } + Id on Class with the left product endofunctor C2 × Id on Class: simply let σ2 be a class function from Seq C2 to { } + (C2 × Seq C2 ) such that for every s ∈ Seq C2,

–  –  –

Now, we can use f to give Seq C1 the structure of a ({ } + (C2 × Id))-coalgebra as well:

just let σ1 be a class function from Seq C1 to { } + (C2 × Seq C1 ) such that for every s ∈ Seq C1,

–  –  –

All our definition says then is that Seq f is a homomorphism from Seq C1, σ1 to Seq C2, σ2. And the existence and uniqueness of this homomorphism follows from the fact that Seq C2, σ2 is actually final in ({ } + (C2 × Id))-Coalg, as the reader may wish to prove.

With experience, all this can be inferred immediately by simple inspection of the form of the defining equations. More importantly, the same type of argument can be applied to the case of any endofunctor, even if there is no readily available representation of a final coalgebra amenable to inductive reasoning (see [44]). A definition that relies in this way on the finality of the implicit target coalgebra is what we call a definition by corecursion. This particular use of the term appears to have originated with [11], and is justified by the duality to the more familiar notion of definition by recursion, which, in similar fashion, relies on the initiality of the implicit source algebra (see [28]).

We can now compose Seq with the left product endofunctor L × Id on Class to obtain the CHAPTER 3. EXECUTION SYSTEMS 54 endofunctor Seq ◦ (L × Id) on Class, which assigns to every class C the class

–  –  –

Finally, we can compose Pow with Seq ◦(L × Id) to obtain the endofunctor Pow ◦ Seq ◦ (L × Id) on Class, which assigns to every class C the class

–  –  –

Just as we did with transition systems, we can take now advantage of the formal analogy between the concepts of binary relation and set-valued function, and use Proposition 2.2.1 to obtain our coalgebraic representation. This unity of treatment is the reward of our aforementioned formalization choice.

By Proposition 2.2.1 then, an L-labelled execution system S, E can be represented as a (Pow ◦ Seq ◦ (L × Id))-coalgebra, namely as S, fun E, and conversely, a (Pow ◦ Seq ◦ (L × Id))-coalgebra C, ε can be represented as an L-labelled execution system, namely as C, rel ε, again with the caveat that C be a set.

For every ordered pair x, y, we write first x, y for x, and sec x, y for y.


–  –  –

At this stage, we could already use Proposition 3.2.4 below as our definition of bisimulation between labelled execution systems. But we prefer a different, more operational one that will help us develop some insight into the concept. And for this, we need some more preparation.

Assume a binary class relation R : C1 ↔ C2.

We write Seq(L × R) for a binary class relation between Seq(L × C1 ) and Seq(L × C2 ) such that for every e1 ∈ Seq(L × C1 ) and every e2 ∈ Seq(L × C2 ),

–  –  –

Seq(L × R) is a simple lift of R to pairs of sequences over dom R and cod R. Informally, if c0, c1,... is a sequence over dom R, and c0, c1,... a sequence over cod R, then

–  –  –

if and only if c0 R c0, c1 R c1, etc. This is, of course, an abuse of notation. But it is a very mild form of abuse. For if R is actually a class function, then Seq(L × R) is the same as the image of R under Seq ◦(L × Id).

Assume L-labelled execution coalgebras C1, ε1 and C2, ε2.

Proposition 3.2.2. B is a bisimulation between C1, ε1 and C2, ε2 if and only if B is a binary class relation between C1, ε1 and C2, ε2, and for any c1 and c2 such that c1 B c2,

the following are true:

–  –  –

Proof. Suppose that B is a bisimulation between C1, ε1 and C2, ε2.

Let graph B, β be an L-labelled execution coalgebra such that dpr B is a homomorphism from graph B, β to C1, ε1, and cpr B one from graph B, β to C2, ε2.

Assume c1 and c2 such that c1 B c2.

Then Pow Seq(L × dpr B)(β( c1, c2 )) = ε1 ((dpr B)( c1, c2 )), and hence, by definition of Pow ◦ Seq ◦ (L × Id) and dpr B, {Seq(L × dpr B)(e) | e ∈ β( c1, c2 )} = ε1 (c1 ).

Thus, by generalization, B is a bisimulation between C1, ε1 and C2, ε2.

Proposition 3.2.2 has the same feel as Proposition 2.2.14. The difference is that the local check of correspondence of transitions has been replaced by a non-local test of agreement along entire executions. This is conceptually in tune with our intended change in scale of observation from one type of system to the other.

Assume L-labelled execution systems S1, E1 and S2, E2.

Definition 3.2.3. A bisimulation between S1, E1 and S2, E2 is a binary relation

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

–  –  –

The following is of course immediate:

Proposition 3.2.4. B is a bisimulation between S1, E1 and S2, E2 if and only if B is a bisimulation between the L-labelled execution coalgebras S1, fun E1 and S2, fun E2.

–  –  –

We say that B is a bisimulation equivalence on S, E if and only if B is a bisimulation on S, E, and an equivalence relation on S.

We say that s1 and s2 are bisimilar among S1, E1 and S2, E2 if and only if there is a bisimulation B between S1, E1 and S2, E2 such that s1 B s2.

We say that s1 and s2 are bisimilar in S, E if and only if s1 and s2 are bisimilar among S, E and S, E.

3.3 Abrahamson systems Informally, we can explain bisimilarity of states of labelled execution systems in the same way as we did in the case of labelled transition systems. Only now, paths are not implicitly inferred from a transition relation, but explicitly stipulated as part of the system structure.

And this can have some peculiar side effects.

For example, consider two {l1, l2 }-labelled execution systems, whose executions are as

depicted in the following left and right frames respectively:

–  –  –

Then s1 and s1 are not bisimilar among the two systems, simply because the execution starting from s2 carries a different label than the one starting from s1. But why should we care if it does? The only execution starting from s1 has only one step, labelled l1, and is in perfect agreement with the only execution starting from s1, which also has only one step, also labelled l1. So, intuitively, there is no difference in branching potential between the two states. We must therefore conclude that bisimilarity is, in this case, inconsistent with our informal sense of equivalence of branching structure.

Pages:     | 1 |   ...   | 4 | 5 || 7 | 8 |   ...   | 12 |

Similar works:

«KRITIKE VOLUME NINE NUMBER TWO (DECEMBER 2015) 193-206 Article Not Even to Know That You Do Not Know: Cicero and the “Theatricality” of the New Academy Soumick De Abstract: The relation between philosophy and theatre has mostly been an ambiguous one, frequently informed with a certain playful irony. Plato’s aversion to include the tragic poets in his Republic, which itself remains a philosophical work written in the dramatic form of dialogues, testifies to this traditional ambiguity. It...»

«On the Dynamic Multiple Intelligence Informed Personalization of the Learning Environment A thesis submitted to the University of Dublin, Trinity College for the degree of Doctor of Philosophy Declan Kelly Department of Computer Science University of Dublin, Trinity College, December, 2005 i Declaration The work presented in this thesis is, except where otherwise stated, entirely that of the author and has not been submitted as an exercise for a degree at this or any other university. Signed: _...»

«Community, Place, and Cultural Battles: Associational Life in Central Italy, 1945-1968 Laura J. Hornbake Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the Graduate School of Arts and Sciences COLUMBIA UNIVERSITY Laura J. Hornbake This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License. ABSTRACT Community, Place, and Cultural Battles: Associational Life in Central Italy, 1945-1968 Laura J. Hornbake...»

«MINING PREDICTIVE PATTERNS AND EXTENSION TO MULTIVARIATE TEMPORAL DATA by Iyad Batal BS, University of Damascus, 2005 MS, University of Pittsburgh, 2008 Submitted to the Graduate Faculty of the Kenneth P. Dietrich School of Arts and Sciences in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Computer Science University of Pittsburgh 2012 UNIVERSITY OF PITTSBURGH COMPUTER SCIENCE DEPARTMENT This dissertation was presented by Iyad Batal It was defended on...»

«COUPLED INVISCID-VISCOUS SOLUTION METHODOLOGY FOR BOUNDED DOMAINS: APPLICATION TO DATA CENTER THERMAL MANAGEMENT A Dissertation Presented to The Academic Faculty by Ethan E. Cruz In Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy in the School of Mechanical Engineering Georgia Institute of Technology December 2015 Copyright © 2015 by Ethan E. Cruz COUPLED INVISCID-VISCOUS SOLUTION METHODOLOGY FOR BOUNDED DOMAINS: APPLICATION TO DATA CENTER THERMAL MANAGEMENT...»


«DEPARTMENT OF PHYSICS UNIVERSITY OF JYVÄSKYLÄ RESEARCH REPORT No. 12/2013 IMPROVEMENT OF TIME-OF-FLIGHT SPECTROMETER FOR ELASTIC RECOIL DETECTION ANALYSIS BY MIKKO LAITINEN Academic Dissertation for the Degree of Doctor of Philosophy To be presented, by the permission of the Faculty of Mathematics and Natural Sciences for the University of Jyväskylä for public examination in Auditorium FYS1 of the University of Jyväskylä on December 20th, 2013 at 12 o’clock noon Jyväskylä, Finland...»

«Methods for Analyzing Early Stage Naval Distributed Systems Designs, Employing Simplex, Multislice, and Multiplex Networks by Douglas Tait Rigterink A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Naval Architecture and Marine Engineering) in The University of Michigan Doctoral Committee: Assistant Professor David J. Singer, Chair Assistant Professor Matthew Collette Professor Scott Page Professor Nickolas Vlahopoulos We sweat like...»

«Masterarbeit zur Erlangung des akademischen Grades Master of Arts der Philosophischen Fakultät der Universität Zürich Die Hausnamen der Schaffhauser Altstadt Verfasserin: Linda Hatt Matrikel-Nr.: 08-716-896 Referentin: Prof. Dr. Elvira Glaser Betreuer: Dr. Martin Graf Deutsches Seminar Abgabedatum: 15.12.2014 Masterarbeit Universität Zürich Hausnamen der Schaffhauser Altstadt Deutsches Seminar Linda Hatt Prof. Dr. E. Glaser / Dr. M. Graf Inhaltsverzeichnis 1. EINLEITUNG 1.1. VORWORT...»

«Developing New Catalysts and Methods for Catalyst-transfer Polycondensations (CTP) by Zachary Jacob Bryan A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Chemistry) in the University of Michigan 2015 Doctoral Committee Associate Professor Anne J. McNeil (Chair) Associate Professor Kenichi Kuroda Professor Adam J. Matzger Professor Melanie S. Sanford Zachary Jacob Bryan 2015 Dedication To my mother, father, brother, and wife for...»

«Chaucer’s Dream Visions: Courtliness and Individual Identity Thesis submitted for the degree of Doctor of Philosophy at the University of Leicester by Michael Costas Hagiioannu BA (Leicester) Department of English University of Leicester January 1998 UMI Number: U105139 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...»

«A Quality-aware Cloud Selection Service for Computational Modellers Shahzad Ahmed Nizamani Submitted in accordance with the requirements for the degree of Doctorate of Philosophy The University of Leeds School of Computing July, 2012 ii The candidate confirms that the work submitted is his own, except where work which has formed part of jointly-authored publications has been included. The contribution of the candidate and the other authors to this work has been explicitly indicated below. 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.