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

    2 Citations (Scopus)
    58 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

    Keywords

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

    Fingerprint Dive into the research topics of 'Layered and Collecting NDFS with Subsumption for Parametric Timed Automata'. Together they form a unique fingerprint.

  • 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