BEZDĚK, Peter, Nikola BENEŠ, Ivana ČERNÁ and Jiří BARNAT. On clock-aware LTL parameter synthesis of timed automata. Journal of Logical and Algebraic Methods in Programming. ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH: Elsevier, 2018, vol. 99, Oct, p. 114-142. ISSN 2352-2208. Available from: https://dx.doi.org/10.1016/j.jlamp.2018.05.004. |
Other formats:
BibTeX
LaTeX
RIS
@article{1423692, author = {Bezděk, Peter and Beneš, Nikola and Černá, Ivana and Barnat, Jiří}, article_location = {ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH}, article_number = {Oct}, doi = {http://dx.doi.org/10.1016/j.jlamp.2018.05.004}, keywords = {Parameter Synthesis; Parametric Timed Automata; Linear Temporal Logic}, language = {eng}, issn = {2352-2208}, journal = {Journal of Logical and Algebraic Methods in Programming}, title = {On clock-aware LTL parameter synthesis of timed automata}, url = {https://www.sciencedirect.com/science/article/pii/S2352220817300354}, volume = {99}, year = {2018} }
TY - JOUR ID - 1423692 AU - Bezděk, Peter - Beneš, Nikola - Černá, Ivana - Barnat, Jiří PY - 2018 TI - On clock-aware LTL parameter synthesis of timed automata JF - Journal of Logical and Algebraic Methods in Programming VL - 99 IS - Oct SP - 114-142 EP - 114-142 PB - Elsevier SN - 23522208 KW - Parameter Synthesis KW - Parametric Timed Automata KW - Linear Temporal Logic UR - https://www.sciencedirect.com/science/article/pii/S2352220817300354 L2 - https://www.sciencedirect.com/science/article/pii/S2352220817300354 N2 - The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for Clock-Aware LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which can result in a faster computation. Our technique adapts the ideas of the automata-based approach to Clock-Aware LTL model checking of timed automata. In order to simplify the explanation of our method, we first introduce a parameter synthesis algorithm for timed automata, then we describe method for checking Clock-Aware LTL properties of timed automata and finally we combine these two methods together to provide general parameter synthesis algorithm for Clock-Aware LTL properties. To demonstrate the usefulness of our approach, we provide experimental evaluation and compare the proposed method with the explicit enumeration technique. ER -
BEZDĚK, Peter, Nikola BENEŠ, Ivana ČERNÁ and Jiří BARNAT. On clock-aware LTL parameter synthesis of timed automata. \textit{Journal of Logical and Algebraic Methods in Programming}. ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH: Elsevier, 2018, vol.~99, Oct, p.~114-142. ISSN~2352-2208. Available from: https://dx.doi.org/10.1016/j.jlamp.2018.05.004.
|