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.
Original 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
Publication statusPublished - 2010

Publication series

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

    Fingerprint

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. https://doi.org/10.1007/978-3-642-15297-9_6