APLAS 2024
Tue 22 - Fri 25 October 2024 Kyoto
Fri 25 Oct 2024 09:30 - 10:00 at Yamauchi Hall - Session 1 Chair(s): Wei-Ngan Chin

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.

Fri 25 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

09:00 - 10:30
Session 1APLAS NIER at Yamauchi Hall
Chair(s): Wei-Ngan Chin National University of Singapore
09:00
30m
Talk
Automata-based approach for quantum circuit/program verification
APLAS NIER
Yu-Fang Chen Academia Sinica
Authorizer link Media Attached File Attached
09:30
30m
Talk
Hyper parametric timed CTL
APLAS NIER
Masaki Waga Kyoto University, Étienne André Université Sorbonne Paris Nord; LIPN; CNRS
DOI Pre-print File Attached
10:00
30m
Talk
Compositional Probabilistic Model Checking with String Diagrams of MDPs
APLAS NIER
Ichiro Hasuo National Institute of Informatics, Japan