Timing diagrams: Formalization and algorithmic verification [Book Review]

Journal of Logic, Language and Information 8 (3):323-361 (1999)
  Copy   BIBTEX

Abstract

Timing diagrams are popular in hardware design. They have been formalized for use in reasoning tasks, such as computer-aided verification. These efforts have largely treated timing diagrams as interfaces to established notations for which verification is decidable; this has restricted timing diagrams to expressing only regular language properties. This paper presents a timing diagram logic capable of expressing certain context-free and context-sensitive properties. It shows that verification is decidable for properties expressible in this logic. More specifically, it shows that containment of -regular languages generated by Büchi automata in timing diagram languages is decidable. The result relies on a correlation between timing diagram and reversal bounded counter machine languages.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-01-28

Downloads
30 (#459,346)

6 months
2 (#668,348)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

The Mathematical Theory of Context Free Languages.Seymour Ginsburg - 1968 - Journal of Symbolic Logic 33 (2):300-301.

Add more references