  Hyperproperties enable simultaneous reasoning about multiple execution traces
of a system and are useful to reason about non-interference, opacity,
robustness, fairness, observational determinism, etc. We introduce hyper
parametric timed computation tree logic (HyperPTCTL), extending hyperlogics
with timing reasoning and, notably, parameters to express unknown values. We
mainly consider its nest-free fragment, where temporal operators cannot be
nested. However, we allow extensions that enable counting actions and comparing
the duration since the most recent occurrence of specific actions. We show that
our nest-free fragment with this extension is sufficiently expressive to encode
properties, e.g., opacity, (un)fairness, or robust observational
(non-)determinism. We propose semi-algorithms for model checking and synthesis
of parametric timed automata (an extension of timed automata with timing
parameters) against this nest-free fragment with the extension via reduction to
PTCTL model checking and synthesis. While the general model checking (and thus
synthesis) problem is undecidable, we show that a large part of our extended
(yet nest-free) fragment is decidable, provided the parameters only appear in
the property, not in the model. We also exhibit additional decidable fragments
where parameters within the model are allowed. We implemented our
semi-algorithms on top of the IMITATOR model checker, and performed
experiments. Our implementation supports most of the nest-free fragments
(beyond the decidable classes). The experimental results highlight our method's
practical relevance.
