Model checking timed systems with urgencies

Pao Ann Hsiung, Shang Wei Lin, Yean Ru Chen, Chun Hsian Huang, Jia Jen Yeh, Hong Yu Sun, Chao Sheng Lin, Hsiao Win Liao

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

3 Citations (Scopus)


Computation tree logic (CTL) model checkers either allow modeling of only lazy semantics in the timed system model or consider at most a simple as soon as possible semantics. However, the design of real-time systems requires different types of urgencies, which have been modeled by several urgency variants of the timed automata model. Except for the IF toolset that model checks timed automata with urgency against observers, the urgency variants of timed automata have not yet been used for verifying the satisfaction of CTL properties in real-time systems. This work is targeted at proposing a zone-based urgency semantics that is time-reactive and at model checking timed automata models that have been extended with such urgency semantics for delayable and eager transition types. Interactions among these different types of transition urgencies are also investigated. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings
PublisherSpringer Verlag
Number of pages15
ISBN (Print)3540472371, 9783540472377
Publication statusPublished - 2006
Event4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 - Beijing, China
Duration: 2006 Oct 232006 Oct 26

Publication series

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


Other4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Model checking timed systems with urgencies'. Together they form a unique fingerprint.

Cite this