Reachability for Multi-Priced Timed Automata with Positive and Negative Rates
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910542006845440 |
|---|---|
| author | Scoones, Andrew Shirmohammadi, Mahsa Worrell, James |
| author_facet | Scoones, Andrew Shirmohammadi, Mahsa Worrell, James |
| contents | Multi-priced timed automata (MPTA) are timed automata with observer
variables whose derivatives can change from one location to another.
Observers are write-only variables, that is, they do not affect the control
flow of the automaton; thus MPTA lie between timed and hybrid
automata in expressiveness. Previous work considered observers with
non-negative slope in every location. In this paper we treat
observers that have both positive and negative rates. Our
main result is an algorithm to decide a gap version of the
reachability problem for this variant of MPTA. We translate the
gap reachability problem into a gap satisfiability problem for mixed
integer-real systems of nonlinear constraints. Our main technical
contribution -- a result of independent interest -- is a procedure
to solve such contraints via a combination of branch-and-bound
and relaxation-and-rounding. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_18131 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Reachability for Multi-Priced Timed Automata with Positive and Negative Rates Scoones, Andrew Shirmohammadi, Mahsa Worrell, James Formal Languages and Automata Theory F.1.1 Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are write-only variables, that is, they do not affect the control flow of the automaton; thus MPTA lie between timed and hybrid automata in expressiveness. Previous work considered observers with non-negative slope in every location. In this paper we treat observers that have both positive and negative rates. Our main result is an algorithm to decide a gap version of the reachability problem for this variant of MPTA. We translate the gap reachability problem into a gap satisfiability problem for mixed integer-real systems of nonlinear constraints. Our main technical contribution -- a result of independent interest -- is a procedure to solve such contraints via a combination of branch-and-bound and relaxation-and-rounding. |
| title | Reachability for Multi-Priced Timed Automata with Positive and Negative Rates |
| topic | Formal Languages and Automata Theory F.1.1 |
| url | https://arxiv.org/abs/2407.18131 |