Advertisement

Language containment of non-deterministic Ω-automata

  • Serdar TaŞiran
  • Ramin Hojati
  • Robert K. Brayton
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

Algorithms and techniques to determinize and complement Ω-automata with various forms of fairness constraints are investigated and implemented. A tool-box is constructed by supplementing these algorithms with less complex ones for certain special cases. Recently published constructions which are asymptotically optimum constitute some of the core routines. The principal use of these tools is in checking language containment between two non-deterministic automata. In language containment based verification, the need for this check may arise in two occasions: when checking whether a system satisfies a property expressed as a non-deterministic automaton, or, in hierarchical verification, where the more detailed system description must satisfy the more abstract specification.

We give examples motivating the utility of non-deterministic specifications and complexity results relating non-deterministic and deterministic Ω-automata. The algorithms mentioned have been implemented as part of the HSIS verification system. Experimental results are presented to demonstrate the practical applicability of the algorithms.

Keywords

Transition Relation Input String Input Symbol Simulation Relation Fairness Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [Cho74]
    Y. Choueka. Theories of Automata on Ω-Tapes: A Simplified Approach. Journal of Computer and System Sciences, 8:117–141, 1974.Google Scholar
  2. [SVW87]
    A.P. Sistla, M.Y. Vardi and P. Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic. Theoretical Computer Science, 49:217–237, 1987.Google Scholar
  3. [Kur87]
    R. P. Kurshan. Reducibility in Analysis of Coordination. In Discrete Events Systems: Models and Applications, volume 103 of LINCS, pages 19–39, 1987Google Scholar
  4. [Lin91]
    B. Lin. Synthesis of VLSI Designs with Symbolic Techniques. Ph.D. thesis, University of California, Berkeley, 1991.Google Scholar
  5. [Saf89]
    S. Safra. Complexity of Automata on Infinite Objects. Ph.D. thesis, The Weizman Institute of Science, Rehovot, Israel, March 1989.Google Scholar
  6. [Saf88]
    S. Safra. On the Complexity of Ω-Automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319–327, 1988.Google Scholar
  7. [SV89]
    S. Safra, and M.Y. Vardi On Ω-Automata and Temporal Logic. In Proc. 21st ACM Symp. on Theory of Computing, 1989.Google Scholar
  8. [Kur92]
    R. P. Kurshan Automata-Theoretic Verification of Coordinating Processes. UC Berkeley Lecture Notes, 1992.Google Scholar
  9. [Saf92]
    S. Safra. Exponential Determinization for Ω-Automata with Strong-Fairness Acceptance Conditions. In Proc. 24th ACM Symposium on Theory of Computing, 1992.Google Scholar
  10. [Saf93]
    S. Safra. Private Communication.Google Scholar
  11. [Cer92]
    E. Cerny. Verification of I/O Trace Set Inclusion for a Class of Nondeterministic Finite State Machines. In Proc. Int'l Conference on Computer Design, Cambridge, pages 526–529, October 1992.Google Scholar
  12. [DHW91]
    D. L. Dill, A. J. Hu and H. Wong-Toi Checking for Language Inclusion Using Simulation Preorders. In Proc. of the Third Workshop on Computer-Aided Verification, 1991.Google Scholar
  13. [HB95]
    R. Hojati and R. K. Brayton Computing Fair Simulation Relations. Unpublished manuscript.Google Scholar
  14. [HSIS94]
    A. Aziz, F. Balarin, R. K. Brayton, S.-T. Cheng, R. Hojati, T. Kam, S. C. Krishnan, R. K. Ranjan A. L. Sangiovanni-Vincentelli T. R. Shiple V. Singhal, S. TaŞiran, H.-Y. Wang. HSIS: A BDD-Based Environment for Formal Verification. In Proc. of the Design Automation Conf., June 1994.Google Scholar
  15. [TaŞ95]
    S. TaŞiran Language Containment Using Non-deterministic Ω-Automata. M.S. thesis, University of California, Berkeley, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Serdar TaŞiran
    • 1
  • Ramin Hojati
    • 1
  • Robert K. Brayton
    • 1
  1. 1.Department of Electrical Engineering and Computer SciencesUniversity of CaliforniaBerkeley

Personalised recommendations