On reachability for hybrid automata over bounded time
This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within T time units, where T is a constant rational value. We show that, in contrast to the classical (unbounded) rea...
| Main Authors: | , , , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2011
|
| _version_ | 1826277565793304576 |
|---|---|
| author | Brihaye, T Doyen, L Geeraerts, G Ouaknine, J Raskin, J Worrell, J |
| author_facet | Brihaye, T Doyen, L Geeraerts, G Ouaknine, J Raskin, J Worrell, J |
| author_sort | Brihaye, T |
| collection | OXFORD |
| description | This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within T time units, where T is a constant rational value. We show that, in contrast to the classical (unbounded) reachability problem, the timed-bounded version is decidable for rectangular hybrid automata provided only non-negative rates are allowed. This class of systems is of practical interest and subsumes, among others, the class of stopwatch automata. We also show that the problem becomes undecidable if either diagonal constraints or both negative and positive rates are allowed. © 2011 Springer-Verlag. |
| first_indexed | 2024-03-06T23:30:50Z |
| format | Journal article |
| id | oxford-uuid:6bf5c3e6-183e-45e6-b93b-34993ddbc02a |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T23:30:50Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | oxford-uuid:6bf5c3e6-183e-45e6-b93b-34993ddbc02a2022-03-26T19:07:42ZOn reachability for hybrid automata over bounded timeJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:6bf5c3e6-183e-45e6-b93b-34993ddbc02aEnglishSymplectic Elements at Oxford2011Brihaye, TDoyen, LGeeraerts, GOuaknine, JRaskin, JWorrell, JThis paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within T time units, where T is a constant rational value. We show that, in contrast to the classical (unbounded) reachability problem, the timed-bounded version is decidable for rectangular hybrid automata provided only non-negative rates are allowed. This class of systems is of practical interest and subsumes, among others, the class of stopwatch automata. We also show that the problem becomes undecidable if either diagonal constraints or both negative and positive rates are allowed. © 2011 Springer-Verlag. |
| spellingShingle | Brihaye, T Doyen, L Geeraerts, G Ouaknine, J Raskin, J Worrell, J On reachability for hybrid automata over bounded time |
| title | On reachability for hybrid automata over bounded time |
| title_full | On reachability for hybrid automata over bounded time |
| title_fullStr | On reachability for hybrid automata over bounded time |
| title_full_unstemmed | On reachability for hybrid automata over bounded time |
| title_short | On reachability for hybrid automata over bounded time |
| title_sort | on reachability for hybrid automata over bounded time |
| work_keys_str_mv | AT brihayet onreachabilityforhybridautomataoverboundedtime AT doyenl onreachabilityforhybridautomataoverboundedtime AT geeraertsg onreachabilityforhybridautomataoverboundedtime AT ouakninej onreachabilityforhybridautomataoverboundedtime AT raskinj onreachabilityforhybridautomataoverboundedtime AT worrellj onreachabilityforhybridautomataoverboundedtime |