Information Technology Reference
In-Depth Information
quotient operation could perhaps be used to synthesise a scheduler for such
problems.Itwouldalsobeofinteresttoaddstochasticfeaturestothemodel.
In[33,25],wehaveproposedamodelwhichtakesadvantagesofbothinterface
automataandmodalspecifications.Oneshouldfollowasimilardirectioninthe
timedsettingandcombineourmodelwiththeoneproposedin [7,6].
Finally,ournotionoferrorstatesisstillprimitiveandinthefutureweplan
to allow the users to define their own error states. This will be done with the
helpofsometemporallogic,justlikeitwasdoneforarefinementin [8].
References
1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2),
183-235 (1994)
2. Alur, R.,Fix, L.,Henzinger, T.A.: Event-clock automata: A determinizable class
oftimedautomata.TheoreticalComputerScience211,1-13(1999)
3. Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.:
Uppaal-tiga: Time for playing games? In: Damm, W., Hermanns, H. (eds.) CAV
2007.LNCS,vol.4590,pp.121-125. Springer,Heidelberg(2007)
4. Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Pettersson, P., Yi, W.,
Hendriks, M.: Uppaal 4.0. In: QEST, pp. 125-126. IEEE Computer Society, Los
Alamitos(2006)
5. Berendsen, J., Vaandrager, F.W.: Compositional abstraction in real-time model
checking. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp.
233-249. Springer,Heidelberg(2008)
6. Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.-B.: A compositional approach
onmodalspecificationsfortimedsystems.In:Breitman,K.,Cavalcanti,A.(eds.)
ICFEM2009.LNCS,vol.5885,Springer,Heidelberg(2009)
7. Bertrand, N., Pinchinat, S., Raclet, J.-B.: Refinement and consistency of timed
modalspecifications.In:Dediu,A.H.,Ionescu,A.M.,Mart´ın-Vide,C.(eds.)LATA
2009.LNCS,vol.5457,pp.152-163. Springer,Heidelberg(2009)
8. Bulychev,P.,Chatain,T.,David,A.,Larsen,K.G.:Ecienton-the-flyalgorithm
for checking alternating timed simulation. In: Ouaknine, J., Vaandrager, F.W.
(eds.)FORMATS2009.LNCS,vol.5813,pp.73-87.Springer,Heidelberg(2009)
9. Cassez,F.,David,A.,Fleury,E.,Larsen,K.G.,Lime,D.:Ecienton-the-flyalgo-
rithmsfortheanalysisoftimedgames.In:Abadi,M.,deAlfaro,L.(eds.)CONCUR
2005.LNCS,vol.3653,pp.66-80.Springer,Heidelberg(2005)
10. Cer¯ans,K.,Godskesen,J.C.,Larsen,K.G.:Timedmodalspecification-theoryand
tools.In:Courcoubetis,C.(ed.)CAV1993.LNCS,vol.697,pp.253-267.Springer,
Heidelberg(1993)
11. Chakabarti,A.,deAlfaro,L.,Henzinger,T.A.,Stoelinga,M.I.A.:Resourceinter-
faces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117-133.
Springer,Heidelberg(2003)
12. David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: Timed I/O au-
tomata: a complete specification theory for real-time systems. In: HSCC (2010)
(accepted)
13. de Alfaro, L., Faella, M.: An accelerated algorithm for 3-color parity games with
an application to timed games. In: Damm, W., Hermanns, H. (eds.) CAV 2007.
LNCS,vol.4590,pp.108-120. Springer,Heidelberg(2007)
