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

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