Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 30
Текст из файла (страница 30)
The partition of the composition's locally-controlled actions is formed by taking the union of thecomponents' partitions (that is, each equivalence class of each component becomes an equivalence class of the composition).Three basic results relate the executions, schedules, and behaviors of a composition tothose of the composition's components. The rst says, for example, that an execution ofa composition induces executions of the component automata. Given an execution =s~01s~1 : : : of A, let jAi be the sequence obtained by deleting j s~j when j is not an actionof Ai and replacing the remaining s~j by s~j i].Proposition6 Let fA g 2I be a strongly compatible collection of automata and let A =Q A .
If 2 execs (Ai) ithenjAi 2 execs (Ai) for every i 2 I . Moreover, the same resulti2I iholds if execs is replaced by it nexecs scheds, nscheds, behs, or nbehs.Here start (A) and states (A) are dened in terms of the ordinary Cartesian product, while sig (A) isdened in terms of the composition of actions signatures just dened. Also, we use the notation ~si] todenote the ith component of the state vector ~s.8147Certain converses of the preceding proposition are also true.
The following propositionsays that executions of component automata can often be pasted together to form an execution of the composition.Proposition7 Let fAigi2I be a strongly compatible collection of automata and let A =Q A . Suppose is anexecution of Ai for every i 2 I , and suppose is a sequence ofii2I iactions in acts (A) such that jAi = sched (i ) for every i 2 I .
Then there is an execution of A such that = sched () and i = jAi for every i 2 I . Moreover, the same result holdswhen acts and sched are replaced by ext and beh, respectively.As a corollary, schedules and behaviors of component automata can also be pasted togetherto form schedules and behaviors of the composition.Proposition8 Let fAigi2I be a strongly compatible collection of automata and let A =Q A . Let be a sequenceof actions in acts (A). If jAi 2 scheds (Ai ) for every i 2 I ,i2I ithen 2 scheds (A).
Moreover, the same result holds when acts and scheds are replaced byext and behs, respectively.As promised, we now dene an operation that `hides' actions of an automaton by converting them to internal actions. This operation is useful for redening what the externalactions of a composition are. We begin with a hiding operation for action signatures: ifS is an action signature and ' acts (S ), then hide S = S 0 where in (S 0) = in (S ) ; ',out (S 0) = out (S ) ; ' and int (S 0) = int (S ) '.
We now dene a hiding operation for automata: if A is an automaton and ' acts (A), then hide A is the automaton A0 obtainedfrom A by replacing sig (A) with sig (A0) = hide sig (A).FairnessWe are in general only interested in the executions of a composition in which all componentsare treated fairly.
While what it means for a component to be treated fairly may vary fromcontext to context, it seems that any reasonable denition should have the property thatinnitely often the component is given the opportunity to perform one of its locally-controlledactions. In this section we dene such a notion of fairness.As we have mentioned, the partition of an automaton's locally-controlled actions is intended to capture some of the structure of the system the automaton is modeling.
Eachclass of actions is intended to represent the set of locally-controlled actions of some systemcomponent.The denition of automaton composition guarantees that an equivalence class of a component automaton becomes an equivalence class of a composition, and hence that compositionretains the essential structure of the system's primitive components.9 In our model, therefore,9It might be argued that retaining this partition is a bad thing to do since it destroys some aspects of148being fair to each component means being fair to each equivalence class of locally-controlledactions.
This motivates the following denition.A fair execution of an automaton A is dened to be an execution of A such that thefollowing conditions hold for each class C of part (A):1. If is nite, then no action of C is enabled in the nal state of .2. If is innite, then either contains innitely many events from C , or containsinnitely many occurrences of states in which no action of C is enabled.This says that a fair execution gives fair turns to each class C of part (A), and therefore toeach component of the system being modeled. Innitely often the automaton attempts toperform an action from the class C . On each attempt, either an action of C is performed, orno action from C can be performed since no action from C is enabled.
For example, we mayview a nite fair execution as an execution at the end of which the automaton repeatedlycycles through the classes in round-robin order attempting to perform an action from eachclass, but failing each time since no action is enabled from the nal state.We denote the set of fair executions of A by fairexecs (A).
We say that is a fair scheduleof A if is the schedule of a fair execution of A, and we denote the set of fair schedulesof A by fairscheds (A). We say that is a fair behavior of A if is the behavior of a fairexecution of A, and we denote the set of fair behaviors of A by fairbehs (A).We can prove the following analogues to Propositions 1-3 in the preceding section:Proposition9 Let fA g be a strongly compatible collection of automata and let A =Q A .
If 2 fairexecsi (Ai2)I then jA 2 fairexecs (A ) for every i 2 I . Moreover, the sameiii2I iresult holds if fairexecs is replaced by fairscheds or fairbehs.Proposition10 Let fAigi2I be a strongly compatible collection of automata and let A =Q A . Suppose is a fairexecution of Ai for every i 2 I , and suppose is a sequence ofii2I iactions in acts (A) such that jAi = sched (i ) for every i 2 I .
Then there is a fair execution of A such that = sched () and i = jAi for every i 2 I . Moreover, the same resultholds when acts and sched are replaced by ext and beh, respectively.Proposition11 Let fAigi2I be a strongly compatible collection of automata and let A =Q A . Let be a sequenceof actions in acts (A). If jAi 2 fairscheds (Ai ) for every i 2 I ,i2I ithen 2 fairscheds (A).
Moreover, the same result holds when acts () and fairscheds () arereplaced by ext and fairbehs, respectively.abstraction. Notice, however, that any reasonable denition of fairness must lead to some breakdown ofabstraction since being fair means being fair to the primitive components which must somehow be modeled.149We state these results because analogous results often do not hold in other models. As wewill see in the following section, the fact that the fair behavior of a composition is uniquelydetermined by the fair behavior of the components makes it possible to reason about thefair behavior of a system in a modular way.1506.852J/18.437J Distributed AlgorithmsLecturer: Nancy LynchOctober 27, 1992Lecture 1313.1 I/O Automata (cont.)13.1.1 Problem SpecicationWe want to say that a problem specication is simply a set of allowable `behaviors,' andthat an automaton solves the specication if each of its `behaviors' is contained in thisset.
The automaton solves the problem in the sense that every `behavior' it exhibits is a`behavior' allowed by the problem specication (but notice that there is no single `behavior'the automaton is required to exhibit). The appropriate notion of `behavior' (e.g., nitebehavior, arbitrary behavior, fair behavior, etc.) used in such a denition depends to someextent on the nature of the problem specication. In addition to a set of allowable behaviors,however, a problem specication must specify the required interface between a solution andits environment.
That is, we want a problem specication to be a set of behaviors togetherwith an action signature.We therefore dene a schedule module H to consist of two components:an action signature sig (H ), anda set scheds (H ) of schedules.Each schedule in scheds (H ) is a nite or innite sequence of actions of H . We denoteby nscheds (H ) the set of nite schedules of H . The behavior of a schedule of H isthe subsequence of consisting of external actions, and is denoted by beh ( ). We saythat is a behavior of H if is the behavior of a schedule of H . We denote the set ofbehaviors of H by behs (H ) and the set of nite behaviors of H by nbehs (H ).
We extendthe denitions of fair schedules and fair behaviors to schedule modules in a trivial way, lettingfairscheds (H ) = scheds (H ) and fairbehs (H ) = behs (H ). We will use the term module torefer to either an automaton or a schedule module.There are several natural schedule modules that we often wish to associate with anautomaton. They correspond to the automaton's schedules, nite schedules, fair schedules, behaviors, nite behaviors and fair behaviors.
For each automaton A, let Scheds (A),151Finscheds (A) and Fairscheds (A) be the schedule modules having action signature sig (A)and having schedules scheds (A), nscheds (A) and fairscheds (A), respectively. Also, foreach module M (either an automaton or schedule module), let Behs (M ), Finbehs (M ) andFairbehs (M ) be the schedule modules having the external action signature extsig (M ) andhaving schedules behs (M ), nbehs (M ) and fairbehs (M ), respectively. (Here and elsewhere,we follow the convention of denoting sets of schedules with lower case names and corresponding schedule modules with corresponding upper case names.)It is convenient to dene two operations for schedule modules. Corresponding to ourcomposition operation for automata, we dene the composition of a countable collectionof strongly compatible schedule modules fHigi2I to be the schedule module H = Qi2I Hiwhere:sig (H ) = Qi2I sig (Hi ),scheds (H ) is the set of sequences of actions of H such that jHi is a schedule of Hifor every i 2 I .The following proposition shows how composition of schedule modules corresponds to composition of automata.Proposition1 Let fA g be a strongly compatible collection of automata and let A =Q A .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
