Model checking prioritized timed automata

Shang Wei Lin, Pao Ann Hsiung, Chun Hsian Huang, Yean-Ru Chen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)

Abstract

Priorities are often used to resolve conflicts in timed systems. However, priorities are not directly supported by state-of-art model checkers. Often, a designer has to either abstract the priorities leading to a high degree of non-determinism or model the priorities using existing primitives. In this work, it is shown how prioritized timed automata can make modelling prioritized timed systems easier through the support for priority specification and model checking. The verification of prioritized timed automata requires a subtraction operation to be performed on two clock zones, represented by DBMs, for which we propose an algorithm to generate the minimal number of zones partitioned. After the application of a series of DBM subtraction operations, the number of zones generated become large. We thus propose an algorithm to reduce the final number of zones partitioned by merging some of them. A typical bus arbitration example is used to illustrate the benefits of the proposed algorithms. Due to the support for prioritization and zone reduction, we observe that there is a 50% reduction in the number of modes and 44% reduction in the number of transitions.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages370-384
Number of pages15
DOIs
Publication statusPublished - 2005 Dec 1
EventThird International Symposium on Automated Technology for Verification and Analysis, ATVA 2005 - Taipei, Taiwan
Duration: 2005 Oct 42005 Oct 7

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3707 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherThird International Symposium on Automated Technology for Verification and Analysis, ATVA 2005
CountryTaiwan
CityTaipei
Period05-10-0405-10-07

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Model checking prioritized timed automata'. Together they form a unique fingerprint.

  • Cite this

    Lin, S. W., Hsiung, P. A., Huang, C. H., & Chen, Y-R. (2005). Model checking prioritized timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 370-384). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3707 LNCS). https://doi.org/10.1007/11562948_28