Cycle encoding-based parameter synthesis for timed automata safety

Sucu B., AYDIN GÖL E.

Acta Informatica, 2024 (SCI-Expanded) identifier identifier

  • Publication Type: Article / Article
  • Publication Date: 2024
  • Doi Number: 10.1007/s00236-024-00460-0
  • Journal Name: Acta Informatica
  • Journal Indexes: Science Citation Index Expanded (SCI-EXPANDED), Scopus, Academic Search Premier, PASCAL, ABI/INFORM, Applied Science & Technology Source, Compendex, Computer & Applied Sciences, INSPEC
  • Middle East Technical University Affiliated: Yes

Abstract

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.