Kaynar D.K., Lynch N., Segala R., Vaandrage F. The Theory of Timed I-O Automata
Подождите немного. Документ загружается.
P1: IML/FFX P2: IML/FFX QC: IML/FFX T1: IML
MOBK015-IND MOBK015-Lynch.cls April 1, 2006 17:6
99
Index
(A, V )-restriction, 17
(A, V )-sequence, 15
abstraction, 2
admissible, 16, 18
algebraic cpo, 9
AlternateA,84
AlternateB,84
Alur–Dill timed automaton, 4
analog variable, 12,22
assume-guarantee, 81
backward simulation, see simulation
relation, 43
BoundedAlternateA,60
BoundedAlternateB,60
CatchUpA, 60, 86
CatchUpB, 60, 86
chain, 9
Clock,63
Clock and manager problem, 63
clock synchronization, 28, 41
ClockSync, 28, 56, 74
compact element of a cpo, 9
comparable, 77
TA, 36
compatible, 79
TA, 53
complete partial order (cpo), 8
algebraic cpo, 9
compact element, 9
composition, 2, 53, 79
continuous, 9
cpo, see complete partial order, 8
discrete action, 19
discrete transition, 19
discrete variable, 12,22
dynamic type, 12
effect, 22
enabled, 19
execution, 29, 74
PeriodicSend,31
Timeout,31
execution fragment, 29, 30, 74
feasible, 36,74
FIN, see finite internal nondeterminism, 34
finite internal nondeterminism (FIN), 34,83
Fischer’s mutual exclusion, 26, 32, 70
FischerME,26
FischerME,70
forward simulation, see simulation relation, 37
clock synchronization, 41
time-bounded channels, 39
hiding, 62
HIOA,3,80
history relation, 46, 47, 78
history variable, 46, 47
time-bounded channels, 46
hybrid automaton, 20, 53
Hybrid I/O Automaton modeling
framework, 3, 91
hybrid sequence, 15, 16
admissible, 16
closed, 16
P1: IML/FFX P2: IML/FFX QC: IML/FFX T1: IML
MOBK015-IND MOBK015-Lynch.cls April 1, 2006 17:6
100 INDEX
hybrid sequence (cont. )
concatenation, 17
limit time, 16
prefix, 16
time-bounded, 16
Zeno, 16
HyTech, 6
I/O feasibility, 90
I/O feasible, 74,89
implementation, 2, 36
invariant, 30
clock agreement, 58
clock validity, 57
ClockSync, 57, 58
failure and timeout, 56
FischerME,32
TimedChannel,32
timeout, 55
Kronos, 5
limit of a chain, 9
linear hybrid automaton, 6
locally Zeno, 74
Manager,63
monotone, 9
non-Zeno, 16, 18
parallel composition, see composition, 2
partial order, 8
complete partial order, 8
periodic sending process, 23, 31
periodic sending process with failures, 24
PeriodicSend, 23, 55
PeriodicSend2, 24, 55
point trajectory, see trajectory, 13
precondition, 22
prefix, 8
progressive, 75,77
prophecy relation, 50,78
prophecy variable, 50
reachable, 30
receptive, 77, 90
receptiveness, 3, 76, 90
refinement, 42
sequence, 8
simulation relation, 2, 37
backward simulation, 37, 43, 45, 78
forward simulation, 37,77
refinement, 42
Specification,63
static type, 11
strategy, 76, 76
substitutivity, 58, 60, 80, 81
System,63
TA, see timed automaton, 19
TA with bounds, 63, 65
task, 63, 65
lower bound, 66
upper bound, 66
time axis, 11
time interval, 11
closed, 11
left-closed, 11
right-closed, 11
time-bounded channel, 23, 32, 39, 47
timed automaton (TA), 19
timed automaton model, 19
Timed I/O automaton (TIOA), 2, 73
Timed Input/Output Automaton modeling
framework, 2
TimedChannel, 23, 55, 74
Timeout,55
Timeout, 24, 55
timeout process, 24, 31
timing-independent, 36,83
TIOA, see Timed I/O automaton, 2
P1: IML/FFX P2: IML/FFX QC: IML/FFX T1: IML
MOBK015-IND MOBK015-Lynch.cls April 1, 2006 17:6
INDEX 101
trace, 2, 30, 74
PeriodicSend,31
Timeout,32
trace fragment, 30, 74
trajectory, 13, 19
closed, 13
concatenation, 14, 15
full, 13
limit time, 14
open, 13
point trajectory, 13,16
prefix, 14
Uppaal, 5
UseNewInputA,86
UseNewInputB,86
UseOldInputA,86
UseOldInputB,86
variables, 11, 13, 19
analog, 12
discrete, 12
dynamic types, 12
static type, 11
weak isomorphism, 42
Zeno, 3, 16, 33
P1: IML/FFX P2: IML/FFX QC: IML/FFX T1: IML
MOBK015-IND MOBK015-Lynch.cls April 1, 2006 17:6
102