2014/09/12 by Peter Bezděk, Bezděk, Peter, Nikola Beneš +5
Chemistry · Computer Science · #68Q60 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Synthetic Organic Chemistry Methods
paper · pdf · doi:10.48550/arxiv.1409.3696
openalex publication_date 2014/09/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The parameter synthesis problem for parametric 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 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 results in a faster computation. Our technique extends the ideas of the automata-based approach to LTL model checking of timed automata. To justify the usefulness of our approach, we provide experimental evaluation and compare our method with explicit enumeration technique.