IEICE TRANSACTIONS on Fundamentals
A Partially Explicit Method for Efficient Symbolic Checking of Language Containment
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E82-A No.11 pp.2455-2464
- Publication Date
- 1999/11/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Kiyoharu HAMAGUCHI, Michiyo ICHIHARA, Toshinobu KASHIWABARA, "A Partially Explicit Method for Efficient Symbolic Checking of Language Containment" in IEICE TRANSACTIONS on Fundamentals,
vol. E82-A, no. 11, pp. 2455-2464, November 1999, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e82-a_11_2455/_p
Copy
@ARTICLE{e82-a_11_2455,
author={Kiyoharu HAMAGUCHI, Michiyo ICHIHARA, Toshinobu KASHIWABARA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={A Partially Explicit Method for Efficient Symbolic Checking of Language Containment},
year={1999},
volume={E82-A},
number={11},
pages={2455-2464},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={November},}
Copy
TY - JOUR
TI - A Partially Explicit Method for Efficient Symbolic Checking of Language Containment
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2455
EP - 2464
AU - Kiyoharu HAMAGUCHI
AU - Michiyo ICHIHARA
AU - Toshinobu KASHIWABARA
PY - 1999
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E82-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 1999
AB - 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.
ER -
English
