Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point

Michal Konečný; Walid Taha; Ferenc A. Bartha; Jan Duracz; Adam Duracz; Aaron D. Ames

doi:10.1016/j.nahs.2015.10.004

Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point

Michal Konečný, Walid Taha, Ferenc A. Bartha, Jan Duracz, Adam Duracz^*, Aaron D. Ames

^*Corresponding author for this work

Computer Science Research Group

Research output: Contribution to journal › Article › peer-review

18 Citations (Scopus)

185 Downloads (Pure)

Abstract

Even simple hybrid automata like the classic bouncing ball can exhibit Zeno behavior. The existence of this type of behavior has so far forced a large class of simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad-hoc restrictions to circumvent Zeno behavior or to abandon hybrid automata. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independent of the occurrence of a given event. Such an event can then even occur an unbounded number of times. This insight makes it possible to handle some types of Zeno behavior. If the post-Zeno state is defined explicitly in the given model of the hybrid automaton, the computed enclosure covers the corresponding trajectory that starts from the Zeno point through a restarted evolution.

Original language	English
Pages (from-to)	1-20
Number of pages	20
Journal	Nonlinear Analysis : Hybrid Systems
Volume	20
Early online date	2 Dec 2015
DOIs	https://doi.org/10.1016/j.nahs.2015.10.004
Publication status	Published - May 2016

Bibliographical note

© 2015 The Authors. Published by Elsevier Ltd. This is an open access article under the CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/)

Funding: US National Science Foundation (awards NSF-CPS-1136099/1136104); Swedish Knowledge Foundation (KK) and the Center for Researchon Embedded Systems (CERES) (grant 20100314); and EPSRC (grant EP/C01037X/1).

Keywords

hybrid automata
hybrid systems
rigorous computations
validated numerics
Zeno behavior

Access to Document

10.1016/j.nahs.2015.10.004Licence: CC BY-NC-ND 3.0

Hybrid automaton up to and beyond a Zeno point
© 2015 The Authors. Published by Elsevier Ltd. This is an open access article under the CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/)
Final published version, 1.36 MBLicence: CC BY-NC-ND 3.0

Cite this

@article{eaa9d6b6baae4cbc82033bb66751eddf,

title = "Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point",

abstract = "Even simple hybrid automata like the classic bouncing ball can exhibit Zeno behavior. The existence of this type of behavior has so far forced a large class of simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad-hoc restrictions to circumvent Zeno behavior or to abandon hybrid automata. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independent of the occurrence of a given event. Such an event can then even occur an unbounded number of times. This insight makes it possible to handle some types of Zeno behavior. If the post-Zeno state is defined explicitly in the given model of the hybrid automaton, the computed enclosure covers the corresponding trajectory that starts from the Zeno point through a restarted evolution.",

keywords = "hybrid automata, hybrid systems, rigorous computations, validated numerics, Zeno behavior",

author = "Michal Kone{\v c}n{\'y} and Walid Taha and Bartha, {Ferenc A.} and Jan Duracz and Adam Duracz and Ames, {Aaron D.}",

note = "{\textcopyright} 2015 The Authors. Published by Elsevier Ltd. This is an open access article under the CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/) Funding: US National Science Foundation (awards NSF-CPS-1136099/1136104); Swedish Knowledge Foundation (KK) and the Center for Researchon Embedded Systems (CERES) (grant 20100314); and EPSRC (grant EP/C01037X/1).",

year = "2016",

month = may,

doi = "10.1016/j.nahs.2015.10.004",

language = "English",

volume = "20",

pages = "1--20",

journal = "Nonlinear Analysis : Hybrid Systems",

issn = "1751-570X",

publisher = "Elsevier",

}

TY - JOUR

T1 - Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point

AU - Konečný, Michal

AU - Taha, Walid

AU - Bartha, Ferenc A.

AU - Duracz, Jan

AU - Duracz, Adam

AU - Ames, Aaron D.

N1 - © 2015 The Authors. Published by Elsevier Ltd. This is an open access article under the CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/) Funding: US National Science Foundation (awards NSF-CPS-1136099/1136104); Swedish Knowledge Foundation (KK) and the Center for Researchon Embedded Systems (CERES) (grant 20100314); and EPSRC (grant EP/C01037X/1).

PY - 2016/5

Y1 - 2016/5

N2 - Even simple hybrid automata like the classic bouncing ball can exhibit Zeno behavior. The existence of this type of behavior has so far forced a large class of simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad-hoc restrictions to circumvent Zeno behavior or to abandon hybrid automata. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independent of the occurrence of a given event. Such an event can then even occur an unbounded number of times. This insight makes it possible to handle some types of Zeno behavior. If the post-Zeno state is defined explicitly in the given model of the hybrid automaton, the computed enclosure covers the corresponding trajectory that starts from the Zeno point through a restarted evolution.

AB - Even simple hybrid automata like the classic bouncing ball can exhibit Zeno behavior. The existence of this type of behavior has so far forced a large class of simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad-hoc restrictions to circumvent Zeno behavior or to abandon hybrid automata. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independent of the occurrence of a given event. Such an event can then even occur an unbounded number of times. This insight makes it possible to handle some types of Zeno behavior. If the post-Zeno state is defined explicitly in the given model of the hybrid automaton, the computed enclosure covers the corresponding trajectory that starts from the Zeno point through a restarted evolution.

KW - hybrid automata

KW - hybrid systems

KW - rigorous computations

KW - validated numerics

KW - Zeno behavior

UR - http://www.scopus.com/inward/record.url?scp=84947996983&partnerID=8YFLogxK

UR - https://www.sciencedirect.com/science/article/pii/S1751570X15000606?via%3Dihub

U2 - 10.1016/j.nahs.2015.10.004

DO - 10.1016/j.nahs.2015.10.004

M3 - Article

AN - SCOPUS:84947996983

SN - 1751-570X

VL - 20

SP - 1

EP - 20

JO - Nonlinear Analysis : Hybrid Systems

JF - Nonlinear Analysis : Hybrid Systems

ER -

Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point

Abstract

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this