Cycle encoding-based parameter synthesis for timed automata safety

Date

2024-01-01

Author

Sucu, Burkay
Aydın Göl, Ebru

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

98
views

0
downloads

Cite This

Parametric timed automata (PTA) extend timed automata (TA) with parameters instead of fixed timing constraints, providing the flexibility to accommodate uncertainties during the design phase. Once a parametric model is obtained, the next step is finding the optimal parameters such that the resulting TA satisfies the specifications. This paper introduces a new algorithm for determining parameters from safety specifications for PTA with bounded integer parameters and no nested cycles. The algorithm searches for unsafe paths through a depth-first search and generates parameter constraints. In particular, the realizability of simple and cyclic paths are encoded via mixed integer linear programming and non-linear programming problems. Then, the parameter constraints rendering the path unrealizable are derived via quantifier elimination. The accumulated constraints through the depth-first search guarantee that a parameter valuation satisfying these constraints solves the synthesis problem. The results are illustrated over benchmarks.

URI

https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85200050443&origin=inward
https://hdl.handle.net/11511/110683

Collections

Department of Computer Engineering, Article