Informace o publikaci
LTL Parameter Synthesis of Parametric Timed Automata
| Autoři | |
|---|---|
| Rok publikování | 2016 |
| Druh | Článek ve sborníku |
| Konference | Software Engineering and Formal Methods - 14th International Conference, SEFM 2016. |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | 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 |
| Obor | Informatika |
| Klíčová slova | LTL model checking - parameter synthesis - timed automata |
| Popis | 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. |
| Související projekty: |