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].
Search WWH ::




Custom Search