The search functionality is under construction.

Author Search Result

[Author] Michiyo ICHIHARA(1hit)

1-1hit
  • A Partially Explicit Method for Efficient Symbolic Checking of Language Containment

    Kiyoharu HAMAGUCHI  Michiyo ICHIHARA  Toshinobu KASHIWABARA  

     
    PAPER

      Vol:
    E82-A No:11
      Page(s):
    2455-2464

    There are two approaches for formal verification of sequential designs or finite state machines: language containment checking and symbolic model checking. To verify designs of practical size, in these two approaches, designs are represented symbolically, in practice, by ordered binary decision diagrams. In the conventional algorithm for language containment checking, finite automata given as specifications are also represented symbolically. This paper proposes a new method, called partially explicit method for checking language containment. By representing states of finite automata given as specifications explicitly, this method can remove redundant computations, and as a result, provide better performance than the conventional method which uses the product machines of designs and specifications. The experimental results show that this approach is effective in checking language containment symbolically.