Group colloquium: Layered and Collecting NDFS with Subsumption for Parametric Timed Automata

When: Sept. 20, 2018, 15:45-16:45

Where: Cubicus B209

Who: Laure Petrucci

We study the analysis and parameter synthesis problems for Parametric Timed Automata (PTA) with properties in Linear-time Temporal Logic (LTL). We introduce 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.