A Transformation-Based Approach to Implication of GSTE Assertion Graphs
Joint Authors
Yang, Guowu
Hung, William N. N.
Song, Xiaoyu
Guo, Wensheng
Source
Journal of Applied Mathematics
Issue
Vol. 2013, Issue 2013 (31 Dec. 2013), pp.1-7, 7 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2013-07-10
Country of Publication
Egypt
No. of Pages
7
Main Subjects
Abstract EN
Generalized symbolic trajectory evaluation (GSTE) is a model checking approach and has successfully demonstrated its powerful capacity in formal verification of VLSI systems.
GSTE is an extension of symbolic trajectory evaluation (STE) to the model checking of ω-regular properties.
It is an alternative to classical model checking algorithms where properties are specified as finite-state automata.
In GSTE, properties are specified as assertion graphs, which are labeled directed graphs where each edge is labeled with two labeling functions: antecedent and consequent.
In this paper, we show the complement relation between GSTE assertion graphs and finite-state automata with the expressiveness of regular languages and ω-regular languages.
We present an algorithm that transforms a GSTE assertion graph to a finite-state automaton and vice versa.
By applying this algorithm, we transform the problem of GSTE assertion graphs implication to the problem of automata language containment.
We demonstrate our approach with its application to verification of an FIFO circuit.
American Psychological Association (APA)
Yang, Guowu& Hung, William N. N.& Song, Xiaoyu& Guo, Wensheng. 2013. A Transformation-Based Approach to Implication of GSTE Assertion Graphs. Journal of Applied Mathematics،Vol. 2013, no. 2013, pp.1-7.
https://search.emarefa.net/detail/BIM-492316
Modern Language Association (MLA)
Yang, Guowu…[et al.]. A Transformation-Based Approach to Implication of GSTE Assertion Graphs. Journal of Applied Mathematics No. 2013 (2013), pp.1-7.
https://search.emarefa.net/detail/BIM-492316
American Medical Association (AMA)
Yang, Guowu& Hung, William N. N.& Song, Xiaoyu& Guo, Wensheng. A Transformation-Based Approach to Implication of GSTE Assertion Graphs. Journal of Applied Mathematics. 2013. Vol. 2013, no. 2013, pp.1-7.
https://search.emarefa.net/detail/BIM-492316
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-492316