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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)

Abstract

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.
LanguageEnglish
Title of host publicationFormal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings)
EditorsK. Chatterjee, T.A. Henzinger
Place of PublicationBerlin
PublisherSpringer
Pages47-61
ISBN (Print)978-3-642-15296-2
DOIs
StatePublished - 2010

Publication series

NameLecture Notes in Computer Science
Volume6246
ISSN (Print)0302-9743

Fingerprint

Hybrid systems
Trajectories
Clocks
Semantics
Chemical analysis

Cite this

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 (Eds.), Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings) (pp. 47-61). (Lecture Notes in Computer Science; Vol. 6246). Berlin: Springer. DOI: 10.1007/978-3-642-15297-9_6
Beek, van, D.A. ; Cuijpers, P.J.L. ; Markovski, J. ; Nadales Agut, D.E. ; Rooda, J.E./ Reconciling urgency and variable abstraction in a hybrid compositional setting. Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings). editor / K. Chatterjee ; T.A. Henzinger. Berlin : Springer, 2010. pp. 47-61 (Lecture Notes in Computer Science).
@inproceedings{7133657dc1c84aa5851524aeb07e9b62,
title = "Reconciling urgency and variable abstraction in a hybrid compositional setting",
abstract = "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.",
author = "{Beek, van}, D.A. and P.J.L. Cuijpers and J. Markovski and {Nadales Agut}, D.E. and J.E. Rooda",
year = "2010",
doi = "10.1007/978-3-642-15297-9_6",
language = "English",
isbn = "978-3-642-15296-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "47--61",
editor = "K. Chatterjee and T.A. Henzinger",
booktitle = "Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings)",
address = "Germany",

}

Beek, van, DA, Cuijpers, PJL, Markovski, J, Nadales Agut, DE & Rooda, JE 2010, Reconciling urgency and variable abstraction in a hybrid compositional setting. in K Chatterjee & TA Henzinger (eds), Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings). Lecture Notes in Computer Science, vol. 6246, Springer, Berlin, pp. 47-61. DOI: 10.1007/978-3-642-15297-9_6

Reconciling urgency and variable abstraction in a hybrid compositional setting. / Beek, van, D.A.; Cuijpers, P.J.L.; Markovski, J.; Nadales Agut, D.E.; Rooda, J.E.

Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings). ed. / K. Chatterjee; T.A. Henzinger. Berlin : Springer, 2010. p. 47-61 (Lecture Notes in Computer Science; Vol. 6246).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Reconciling urgency and variable abstraction in a hybrid compositional setting

AU - Beek, van,D.A.

AU - Cuijpers,P.J.L.

AU - Markovski,J.

AU - Nadales Agut,D.E.

AU - Rooda,J.E.

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-15297-9_6

DO - 10.1007/978-3-642-15297-9_6

M3 - Conference contribution

SN - 978-3-642-15296-2

T3 - Lecture Notes in Computer Science

SP - 47

EP - 61

BT - Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings)

PB - Springer

CY - Berlin

ER -

Beek, van DA, Cuijpers PJL, Markovski J, Nadales Agut DE, Rooda JE. Reconciling urgency and variable abstraction in a hybrid compositional setting. In Chatterjee K, Henzinger TA, editors, Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings). Berlin: Springer. 2010. p. 47-61. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-15297-9_6