Layered and Collecting NDFS with Subsumption for Parametric Timed Automata

Hoang Gia Nguyen, Laure Petrucci, Jaco van de Pol

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

29 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publication23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018
EditorsAnthony Widjaja Lin, Jun Sun
Place of PublicationIEEE Xplore
PublisherIEEE Canada
Number of pages9
ISBN (Electronic)978-1-5386-9341-4
DOIs
Publication statusPublished - Dec 2018
Event23rd International Conference on Engineering of Complex Computer Systems 2018 - Monash University, Melbourne, Australia
Duration: 12 Dec 201814 Dec 2018
Conference number: 23
http://formal-analysis.com/iceccs/2018/

Conference

Conference23rd International Conference on Engineering of Complex Computer Systems 2018
Abbreviated titleICECCS 2018
CountryAustralia
CityMelbourne
Period12/12/1814/12/18
Internet address

Fingerprint

Temporal logic
Model checking
Experiments

Keywords

  • Parametric Timed Automata
  • Parameter Synthesis
  • nested depth-first search
  • Linear Temporal Logic
  • Timed Büchi Automata

Cite this

Nguyen, H. G., Petrucci, L., & Pol, J. V. D. (2018). Layered and Collecting NDFS with Subsumption for Parametric Timed Automata. In A. W. Lin, & J. Sun (Eds.), 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018 IEEE Xplore: IEEE Canada. https://doi.org/10.1109/ICECCS2018.2018.00009
Nguyen, Hoang Gia ; Petrucci, Laure ; Pol, Jaco van de. / Layered and Collecting NDFS with Subsumption for Parametric Timed Automata. 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018. editor / Anthony Widjaja Lin ; Jun Sun. IEEE Xplore : IEEE Canada, 2018.
@inproceedings{0218b6029de743799e4dafff80fbfb5e,
title = "Layered and Collecting NDFS with Subsumption for Parametric Timed Automata",
abstract = "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.",
keywords = "Parametric Timed Automata, Parameter Synthesis, nested depth-first search, Linear Temporal Logic, Timed B{\"u}chi Automata",
author = "Nguyen, {Hoang Gia} and Laure Petrucci and Pol, {Jaco van de}",
year = "2018",
month = "12",
doi = "10.1109/ICECCS2018.2018.00009",
language = "English",
editor = "Lin, {Anthony Widjaja} and Jun Sun",
booktitle = "23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018",
publisher = "IEEE Canada",
address = "Canada",

}

Nguyen, HG, Petrucci, L & Pol, JVD 2018, Layered and Collecting NDFS with Subsumption for Parametric Timed Automata. in AW Lin & J Sun (eds), 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018. IEEE Canada, IEEE Xplore, 23rd International Conference on Engineering of Complex Computer Systems 2018, Melbourne, Australia, 12/12/18. https://doi.org/10.1109/ICECCS2018.2018.00009

Layered and Collecting NDFS with Subsumption for Parametric Timed Automata. / Nguyen, Hoang Gia; Petrucci, Laure; Pol, Jaco van de.

23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018. ed. / Anthony Widjaja Lin; Jun Sun. IEEE Xplore : IEEE Canada, 2018.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Layered and Collecting NDFS with Subsumption for Parametric Timed Automata

AU - Nguyen, Hoang Gia

AU - Petrucci, Laure

AU - Pol, Jaco van de

PY - 2018/12

Y1 - 2018/12

N2 - 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.

AB - 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.

KW - Parametric Timed Automata

KW - Parameter Synthesis

KW - nested depth-first search

KW - Linear Temporal Logic

KW - Timed Büchi Automata

U2 - 10.1109/ICECCS2018.2018.00009

DO - 10.1109/ICECCS2018.2018.00009

M3 - Conference contribution

BT - 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018

A2 - Lin, Anthony Widjaja

A2 - Sun, Jun

PB - IEEE Canada

CY - IEEE Xplore

ER -

Nguyen HG, Petrucci L, Pol JVD. Layered and Collecting NDFS with Subsumption for Parametric Timed Automata. In Lin AW, Sun J, editors, 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018. IEEE Xplore: IEEE Canada. 2018 https://doi.org/10.1109/ICECCS2018.2018.00009