Cycle encoding-based parameter synthesis for timed automata safety

Sucu B., AYDIN GÖL E.

Acta Informatica, cilt.61, sa.4, ss.333-356, 2024 (SCI-Expanded) identifier identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 61 Sayı: 4
  • Basım Tarihi: 2024
  • Doi Numarası: 10.1007/s00236-024-00460-0
  • Dergi Adı: Acta Informatica
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus, Academic Search Premier, PASCAL, ABI/INFORM, Applied Science & Technology Source, Compendex, Computer & Applied Sciences, INSPEC
  • Sayfa Sayıları: ss.333-356
  • Orta Doğu Teknik Üniversitesi Adresli: Evet

Özet

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.