Timed Automata Relaxation for Reachability
| Authors | |
|---|---|
| Year of publication | 2021 |
| Type | Article in Proceedings |
| Conference | 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21) |
| MU Faculty or unit | |
| Citation | |
| Web | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979188/ |
| Doi | http://dx.doi.org/10.1007/978-3-030-72016-2_16 |
| Keywords | Timed Automata - Reachability - Relaxation of Constraints |
| Description | Timed automata (TA) have shown to be a suitable formalism for modeling real-time systems. Moreover, modern model-checking tools allow a designer to check whether a TA complies with the system specification. However, the exact timing constraints of the system are often uncertain during the design phase. Consequently, the designer is able to build a TA with a correct structure, however, the timing constraints need to be tuned to make the TA comply with the specification. In this work, we assume that we are given a TA together with an existential property, such as reachability, that is not satisfied by the TA. We propose a novel concept of a minimal sufficient reduction (MSR) that allows us to identify the minimal set S of timing constraints of the TA that needs to be tuned to meet the specification. Moreover, we employ mixed-integer linear programming to actually find a tuning of S that leads to meeting the specification. |
| Related projects: |