|
| << vorige | volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 11 van 15 gevonden artikelen
| Titel: |
Parameter Synthesis for Timed Kripke Structures |
| Auteur: |
Knapik, Michał Penczek, Wojciech |
| Verschenen in: |
Fundamenta informaticae |
| Paginering: | Jaargang 133 (2014) nr. 2-3 pagina's 211-226 |
| Jaar: |
2014-09-29 |
| Inhoud: |
We show how to synthesise parameter values under which a given property, expressed in a certain extension of CTL, called RTCTLP, holds in a parametric timed Kripke structure. We prove the decidability of parameter synthesis for RTCTLP by showing how to restrict the infinite space of parameter valuations to its finite subset and employ a brute-force algorithm. The brute-force approach soon becomes intractable, therefore we propose a symbolic algorithm for RTCTLP parameter synthesis. Similarly to the fixed-point symbolic model checking approach, we introduce special operators which stabilise on the solution. The process of stabilisation is essentially a translation from the RTCTLP parameter synthesis problem to a discrete optimization task. We show that the proposed method is sound and complete and provide some complexity results. We argue that this approach leads to new opportunities in model checking, including the use of integer programming and related tools. |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 11 van 15 gevonden artikelen
| << vorige | volgende >> |