Specification and validation of dynamic systems using temporal logic

S. M. Cho, H. H. Kim, S. D. Cha, D. H. Bae

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)


A specification and validation technique for dynamic systems is proposed. In particular, a new temporal logic, called HDTL, is presented and the tableau method revised for automatic analysis. Using a freeze quantifier, HDTL with the revised tableau method makes it possible to specify the correctness requirements of dynamic systems and validate them. The proposed logic is rather generic, i.e. it has only a few assumptions on operational language. The authors introduce a simple dynamic modelling language and illustrate its experiment. The experiment shows that HDTL is suitable for specifying dynamic properties and the analysis technique is promising.

Original languageEnglish
Pages (from-to)135-140
Number of pages6
JournalIEE Proceedings: Software
Issue number4
Publication statusPublished - 2001 Aug
Externally publishedYes

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design


Dive into the research topics of 'Specification and validation of dynamic systems using temporal logic'. Together they form a unique fingerprint.

Cite this