IDEAS home Printed from https://ideas.repec.org/a/hin/jnljam/709071.html
   My bibliography  Save this article

A Transformation-Based Approach to Implication of GSTE Assertion Graphs

Author

Listed:
  • Guowu Yang
  • William N. N. Hung
  • Xiaoyu Song
  • Wensheng Guo

Abstract

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.

Suggested Citation

  • Guowu Yang & William N. N. Hung & Xiaoyu Song & Wensheng Guo, 2013. "A Transformation-Based Approach to Implication of GSTE Assertion Graphs," Journal of Applied Mathematics, Hindawi, vol. 2013, pages 1-7, July.
    • Handle: RePEc:hin:jnljam:709071
    DOI: 10.1155/2013/709071
    as

    Download full text from publisher

    File URL: http://downloads.hindawi.com/journals/JAM/2013/709071.pdf
    Download Restriction: no
    File URL: http://downloads.hindawi.com/journals/JAM/2013/709071.xml
    Download Restriction: no
    File URL: https://libkey.io/10.1155/2013/709071?utm_source=ideas
    LibKey link: if access is restricted and if your library uses this service, LibKey will redirect you to where you can use your library subscription to access this item
    ---><---

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Lisa Coleman, 2022. "Global Inclusion, Diversity, Belonging, Equity, and Access - GIDBEA. The Architecture of A New Different," Academicus International Scientific Journal, Entrepreneurship Training Center Albania, issue 25, pages 91-103, January.

    More about this item

    Statistics

    Access and download statistics

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:hin:jnljam:709071. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    We have no bibliographic references for this item. You can help adding them by using this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Mohamed Abdelhakeem (email available below). General contact details of provider: https://www.hindawi.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.