This paper studies the analysis and parameter synthesis problems for Parametric Timed Automata (PTA) with properties in Linear-time Temporal Logic (LTL). It introduces a series of variations of Nested Depth-First Search (NDFS). We first study the LTL model checking problem for PTA. Based on a careful analysis of parametric zones, we introduce a new layered NDFS approach to LTL model checking. We integrate this with several techniques to prune the search space. In particular, we apply subsumption abstraction to PTA for the first time. We also propose heuristics on the search order to improve the performance. Next, we study parameter synthesis. To this end, this new layered approach and subsumption are added to a Collecting NDFS scheme. We implemented all algorithms in the Imitator tool and analyse their efficiency in a number of experiments.

Parametric timed automata are a powerful formalism to reason about, model and verify real-time systems in which some constraints are unknown, or subject to uncertainty. Parameter synthesis using parametric timed automata is very sensitive to the state space explosion problem. To mitigate this problem, we propose two new exploration orders, i. e., the "ranking strategy" and the "priority based strategy", and compare them with existing strategies. We consider both complete parameter synthesis, and counterexample synthesis where the analysis stops as soon as some parameter valuations are found. Experimental results using IMITATOR show that our new strategies significantly outperform existing approaches, especially in the counterexample synthesis.