Title: Theory / Unimportant / CS / Algo / Distributed Lynch / Asynchronous Network algorithm
Tags: hasSeenConjDef

Name: The signature of an I/O automaton
Definition: A description of input, output and internal actions.
Page: 201
Chapter: 8
Section: 1

Name: The input actions
Page: 201
Chapter: 8
Section: 1
Variables: \(S\) a signature
Abbreviation: \(in(S)\)

Name: The output actions
Page: 201
Chapter: 8
Section: 1
Variables: \(S\) a signature
Abbreviation: \(out(S)\)

Name: The internal actions
Page: 201
Chapter: 8
Section: 1
Variables: \(S\) a signature
Abbreviation: \(int(S)\)

Name: The external actions
Definition: \(out(s)\cup in(S)\)
Page: 201
Chapter: 8
Section: 1
Variables: \(S\) a signature
Abbreviation: \(ext(S)\)

Name: The locally controlled actions
Definition: \(out(s)\cup int(S)\)
Page: 201
Chapter: 8
Section: 1
Variables: \(S\) a signature
Notation: \(local(S)\)

Name: An I/O automaton
Definition: \(sig(A)\)
Page: 201
Chapter: 8
Section: 1
Definition2: \(states(A)\)
Conjdef: A tuple
Definition3: \(start(A)\)
Definition4: \(trans(A)\)
Definition5: \(tasks(A)\)

Name: The signature of \(A\)
Typ: A set
Page: 201
Section: 1
Chapter: 8
Variables: \(A\) an I/O automaton
Abbreviation: \(sig(A)\)

Name: The set of states of \(A\)
Typ: A set (not necessarily finite)
Page: 201
Section: 1
Chapter: 8
Variables: \(A\) an I/O automaton
Notation: \(states(A)\)

Name: The start states of \(A\)
Typ: A subset of \(states(A)\)
Page: 202
Section: 1
Chapter: 8
Variables: \(A\) an I/O automaton
Abbreviation: \(start(A)\)

Name: The state-transition relation of \(A\)
Definition: for every state \(s\) and input action \(\pi\), there is a transition \((s,\pi,s')\in trans(A)\)
Page: 202
Chapter: 8
Section: 1
Variables: \(A\) an I/O automaton
Abbreviation: \(trans(A)\)
DefType: A subset of \(states(A)\times acts(sig(A))\times states(A)\)

Name: The task partition of \(A\)
Typ: An equivalence relation on \(local(sig(A))\) having at most countably many equivalence classes.
Page: 202
Section: 1
Chapter: 8
Variables: \(A\) an I/O automaton
Abbreviation: \(tasks(A)\)

Definition: \(s(sig(A))\)
Page: 202
Chapter: 8
Section: 1
Variables: \(A\) an I/O automaton,
let \(s\) be \(acts\), \(in\), ... a function on signatures
Notation: \(s(A)\)

Name: A transition of \(A\)
Definition: Some \((s,\pi,s')\in tran(A)\)
Page: 202
Chapter: 8
Section: 1
Variables: \(A\) an I/O automaton
Name2: A step of \(A\)

Name: A input/output/... transition of \(A\)
Definition: Some \((s,\pi,s')\in tran(A)\) where \(\pi\) is an input/output/... symbol
Page: 202
Chapter: 8
Section: 1
Variables: \(A\) an I/O automaton

Name: An action enabled in \(s\)
Definition: Some action \(\pi\) such that \((s,\pi,s')\in trans(A)\)
Page: 202
Chapter: 8
Section: 1
Variables: \(A\) an I/O automaton,
\(s\) a state

Name: An input-enabled automaton
Definition: An I/O automaton where input actions are enabled at each state
Page: 202
Chapter: 8
Section: 1

Name: A quiescent state
Definition: A state whose only enabled actions are input
Page: 202
Chapter: 8
Section: 1
Variables: \(A\) an I/O automaton

Question: Why requiring input-enabling property ?
Answer: a serious source of errors in the development of system components is the failure to specify what the component does in the face of unexpected inputs.
Page: 203
Chapter: 8
Section: 1
Context: Asynchronous network
Answer2: use of input-enabling makes the basic theory of the model work out nicely

Name: \(C\) is enabled in \(s\)
Definition: some action in \(C\) is enabled in \(s\)
Page: 203
Chapter: 8
Section: 1
Variables: \(A\) an I/O automaton,
let \(s\) a state,
\(C\) a task

Name: The external signature
Definition: \((in(S),out(S),\emptyset)\)
Page: 201
Chapter: 8
Section: 1
Variables: \(S\) a signature
Name2: The external interface of \(S\)
Abbreviation: \(extsig(S)\)
Typ: A signature