Reconciling urgency and variable abstraction in a hybrid compositional setting

D.A. Beek, van, P.J.L. Cuijpers, J. Markovski, D.E. Nadales Agut, J.E. Rooda

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

5 Citaten (Scopus)

Samenvatting

The extension of timed formalisms to a hybrid setting with urgency, has been carried out in a rather straightforward manner, seemingly without difficulty. However, in this paper, we show that the combination of urgency with abstraction from continuous variables leads to undesired behavior. Abstraction from continuous variables ultimately leads to a timed system again, but with a much richer set of possible branching behaviors than a timed system that comprises only clocks. As it turns out, the formal definition of urgency, as defined for timed systems with clocks, does not fit our intuition of urgency anymore when applied to a timed system that is an abstraction of a hybrid system. Therefore, we propose to extend the formal semantics of timed and hybrid systems with guard trajectories. In this way, the continuous branching behavior introduced by hybrid systems remains visible even after abstraction from continuous variables. The practical applicability of the introduction of guard trajectories is illustrated by our revision of the structured operational semantics of the CIF language. The interplay between urgency and abstraction now adheres to our intuition, while compositionality with respect to urgency, variable abstraction, and parallel composition, is retained. In the future, symbolic elimination of urgency can be used to ensure that guard trajectories do not need to be actually calculated.
Originele taal-2Engels
TitelFormal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings)
RedacteurenK. Chatterjee, T.A. Henzinger
Plaats van productieBerlin
UitgeverijSpringer
Pagina's47-61
ISBN van geprinte versie978-3-642-15296-2
DOI's
StatusGepubliceerd - 2010

Publicatie series

NaamLecture Notes in Computer Science
Volume6246
ISSN van geprinte versie0302-9743

Vingerafdruk Duik in de onderzoeksthema's van 'Reconciling urgency and variable abstraction in a hybrid compositional setting'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Beek, van, D. A., Cuijpers, P. J. L., Markovski, J., Nadales Agut, D. E., & Rooda, J. E. (2010). Reconciling urgency and variable abstraction in a hybrid compositional setting. In K. Chatterjee, & T. A. Henzinger (editors), Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings) (blz. 47-61). (Lecture Notes in Computer Science; Vol. 6246). Springer. https://doi.org/10.1007/978-3-642-15297-9_6