2018/08/21 by Liyun Dai, Dai, Liyun, Bo Liu +5
Computer Science · #FOS: Electrical engineering #Formal Methods in Verification #Logic, programming, and type systems #Petri Nets in System Modeling #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1808.06792
openalex publication_date 2018/08/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider the parameter synthesis problem of parametric timed automata (PTAs). The problem is, given a PTA and a property, to compute the set of valuations of the parameters under which the resulting timed automaton satisfies the property. Such a set of parameter valuations is called a feasible region for the PTA and the property. The problem is known undecidable in general. This paper, however, presents our study on some decidable sub-classes of PTAs and proposes efficient parameter synthesis algorithms for them.