Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2205.04392 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913437440802816 |
|---|---|
| author | Dziadek, Sven Fahrenberg, Uli Schlehuber-Caissier, Philipp |
| author_facet | Dziadek, Sven Fahrenberg, Uli Schlehuber-Caissier, Philipp |
| contents | We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a Büchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm interleaved with Couvreur's algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source platforms TChecker and~Spot. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2205_04392 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | $ω$-Regular Energy Problems Dziadek, Sven Fahrenberg, Uli Schlehuber-Caissier, Philipp Logic in Computer Science We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a Büchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm interleaved with Couvreur's algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source platforms TChecker and~Spot. |
| title | $ω$-Regular Energy Problems |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2205.04392 |