Layered and Collecting NDFS with Subsumption for Parametric Timed Automata

Hoang Gia Nguyen; Laure Petrucci; Jaco van de Pol

doi:10.1109/ICECCS2018.2018.00009

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 proceeding › Conference contribution › Academic › peer-review

11 Citations (Scopus)

165 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 language	English
Title of host publication	23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018
Editors	Anthony Widjaja Lin, Jun Sun
Place of Publication	IEEE Xplore
Publisher	IEEE
Number of pages	9
ISBN (Electronic)	978-1-5386-9341-4
DOIs	https://doi.org/10.1109/ICECCS2018.2018.00009
Publication status	Published - Dec 2018
Event	23rd International Conference on Engineering of Complex Computer Systems 2018 - Monash University, Melbourne, Australia Duration: 12 Dec 2018 → 14 Dec 2018 Conference number: 23 http://formal-analysis.com/iceccs/2018/

Conference

Conference	23rd International Conference on Engineering of Complex Computer Systems 2018
Abbreviated title	ICECCS 2018
Country/Territory	Australia
City	Melbourne
Period	12/12/18 → 14/12/18
Internet address	http://formal-analysis.com/iceccs/2018/

Keywords

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

Access to Document

10.1109/ICECCS2018.2018.00009

PID5576965Accepted author version, 320 KB

Cite this

@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 = dec,

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",

address = "United States",

note = "23rd International Conference on Engineering of Complex Computer Systems 2018, ICECCS 2018 ; Conference date: 12-12-2018 Through 14-12-2018",

url = "http://formal-analysis.com/iceccs/2018/",

}

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, IEEE Xplore, 23rd International Conference on Engineering of Complex Computer Systems 2018, Melbourne, Victoria, 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, 2018.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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

N1 - Conference code: 23

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

CY - IEEE Xplore

T2 - 23rd International Conference on Engineering of Complex Computer Systems 2018

Y2 - 12 December 2018 through 14 December 2018

ER -

Layered and Collecting NDFS with Subsumption for Parametric Timed Automata

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this