LTL Parameter Synthesis of Parametric Timed Automata
| Authors | |
|---|---|
| Year of publication | 2016 |
| Type | Article in Proceedings |
| Conference | Software Engineering and Formal Methods - 14th International Conference, SEFM 2016. |
| MU Faculty or unit | |
| Citation | |
| Web | http://dx.doi.org/10.1007/978-3-319-41591-8_12 |
| Doi | http://dx.doi.org/10.1007/978-3-319-41591-8_12 |
| Field | Informatics |
| Keywords | LTL model checking - parameter synthesis - timed automata |
| Description | The parameter synthesis problem for parametric timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valua- tions under which the parameter synthesis problem is decidable for LTL properties. The investigated bounded integer parameter synthesis prob- lem could be solved using an explicit enumeration of all possible parame- ter valuations. We propose an alternative symbolic zone-based method for this problem which results in a faster computation. Our technique extends the ideas of the automata-based approach to LTL model check- ing of timed automata. To justify the usefulness of our approach, we provide experimental evaluation and compare our method with explicit enumeration technique. |
| Related projects: |