Hyper parametric timed CTL
Masaki Waga, Étienne André
TL;DR
This work introduces HyperPTCTL, a parametric timed hyperlogic for reasoning about multiple execution traces, and its nest-free fragment extended with COUNT and LAST predicates to capture action counts and last-occurrence timing. The authors develop semi-algorithms that reduce Nest-Free Ext-HyperPTCTL model checking and synthesis to Ext-PTCTL via self-composition and observers, enabling existing PTCTL techniques to be reused. They identify decidable subclasses depending on parameter placement (in the property vs in the model) and demonstrate practical feasibility with an implementation (HyPTCTLchecker) built atop IMITATOR, showing favorable results on moderate-size PTAs and properties. The approach supports encoding opacity, (un)fairness, and robust observational nondeterminism in a timed-parametric setting, and experiments indicate the method’s practical relevance, while highlighting areas for further decidable boundaries and optimization. Overall, this work extends hyperlogics into the timed-parametric domain and provides tractable pathways for model checking and synthesis in many useful cases, with a functioning toolchain and empirical validation.
Abstract
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.