Information Technology Reference
In-Depth Information
write
s
−→
S
s
insteadof
(
s, a, s
)
∈
→
S
anduse
i
?
,
o
!
and
d
torangeoverinputs,
outputsand
R
≥
0
respectively.Inaddition anyTIOTSsatisfiesthefollowing:
[timedeterminism]whenever
s
−→
S
s
and
s
−→
S
s
then
s
=
s
[timereflexivity]
s
−→
S
s
forall
s
St
S
∈
St
S
and all
d
1
,d
2
∈
R
≥
0
wehave
s
d
1
+
d
2
[time additivity] for all
s, s
∈
−−−−→
S
s
iff
St
S
s
d
−−→
S
s
and
s
d
2
−−→
S
s
foran
s
∈
TIOTSs are semantic objects that represent timed interactive processes. In
our framework we use
Timed I/O Automata
as a syntactic domain in which
specifications
and
implementations
arerepresented.
Definition 2.
A
TimedI/OAutomaton
(TIOA)isatuple
A
=(
Loc
,q
0
,
Clk
,E,
Act,
Inv
)
whereLocisafinitesetoflocations,
q
0
∈
Locistheinitiallocation,Clk
isafinitesetofclocks,
E
⊆
Loc
×
Act
×B
(
Clk
)
×P
(
Clk
)
×
Locisasetofedges
with
Act
o
is a finite set of
actions,partitionedintoinputsandoutputsrespectively,andInv
:
Loc
B
(
Clk
)
being a set of clock constraints, Act
=
Act
i
⊕
→B
(
Clk
)
isasetoflocation invariants.
As for timed automata,a
state
ofA is a pair
(
q, V
)
where
q
is a location and
V
:
Clk
→
R
≥
0
isa
valuationfunction
thatassignsanon-negativevaluetoeach
clockin
Clk
.Wewrite
u
+
d
todenoteavaluationsuchthatforanyclock
r
we
have
(
u
+
d
)(
r
)=
x
+
d
iff
u
(
r
)=
x
.Given
d
→
0]
r∈c
fora
valuationwhichagreeswith
u
onallvaluesforclocksnotin
c
,andreturns0for
allclocksin
c
.Weuse
0
todenotetheconstantfunctionmappingallclocksto
zero.The
initialstate
of
A
isthepair
(
q
0
,
0
)
.
We visualise TIOAs using classical Timed Automata notation, extending it
withtwotypesoftransitions(inputsandoutputs).SeeexampleinFigure1.
∈
R
≥
0
,wewrite
u
[
r
ThesemanticsofaTIOA
A
=(
Loc
,q
0
,
Clk
,E,
Act
,
Inv
)
isaTIOTS
[[
A
]]
sem
=
(
Loc
×
(
Clk
→
R
≥
0
)
,
(
q
0
,
0
)
,
Act
,
→
)
,where
isthelargesttransitionrelation
→
generatedbythefollowingrules:
-
Each
(
q, a, ϕ, c, q
)
∈
E
givesriseto
(
q, u
)
−→
(
q
,u
)
foreachclockvaluation
|
=
ϕ
and
u
=
u
[
r
→
0]
r∈c
and
u
|
=
Inv
(
q
)
.
u
∈
[
Clk
→
R
≥
0
]
suchthat
u
-
Each location
q
∈
Loc
with a valuation
u
∈
[
Clk
→
R
≥
0
]
gives rise to a
transition
(
q, u
)
−→
(
q, u
+
d
)
foreachdelay
d
∈
R
≥
0
suchthat
u
+
d
|
=
Inv
(
q
)
.
ObservethattheTIOTSsinducedbyaTIOAsnaturallysatisfythethreeaxioms
of Definition 1. In the rest of the paper, we will only consider deterministic
TIOAs,whosecorrespondingTIOTSsaredeterministic.
ATIOTSrepresentsatwo-player
timedgame
[9].The
Input
player(theenvi-
ronment)controlsthe input transitionsofthe TIOTS.The
Output
player(the
system)controlstheoutputtransitions.Theformaldefinitionsofstrategyand
move outcomes for such a game are given in [12]. The set of
winning states
fromwhichoneoftheplayershasastrategytosatisfyasafetyorareachability
objectivecanbecomputedwithalgorithmspresentedin[9]—ecientsymbolic
versionsofwell-knowncontrollersynthesisalgorithmsof[30].