Implementing WS1S via finite automata

  • James Glenn
  • William Gasarch
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1260)


It has long been known that WSIS is decidable through the use of finite automata. However, since the worst-case running time has been proven to grow extremely quickly, few have explored the implementation of the algorithm. In this paper we describe some of the points of interest that have come up while coding and running the algorithm. These points include the data structures used as well as the special features of the automata, which we can exploit to perform minimization very quickly in certain cases. We also present some data that enable us to gain insight into how the algorithm performs in the average case, both on random inputs and on inputs that come from the use of Presburger Arithmetic (which can be converted to WSIS) in compiler optimization.


Decision Procedure Atomic Formula Minimization Algorithm Finite Automaton Tree Automaton 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. R. Büchi. Weak second order arithmetic and finite automata. Zeitscrift fur mathematische Logic und Grundlagen der Mathematik, 6:66–92, 1960.Google Scholar
  2. 2.
    J. Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Z. Kohavi and A. Paz, editors, Theory of Machines and Computation, pages 189–196. Academic Press, 1976.Google Scholar
  3. 3.
    A. R. Meyer. Weak monadic second order theory of successor is not elementary-recursive. In Logic Colloquium, number 453 in Lecture Notes in Mathematics, pages 132–154. Springer-Verlag, 1974.Google Scholar
  4. 4.
    D. C. Oppen. Elementary bounds for Presburger arithmetic. In 5th ACM Symposium on Theory of Computing, pages 34–37, 1973.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • James Glenn
    • 1
  • William Gasarch
    • 2
  1. 1.Department of Computer ScienceUniversity of MarylandCollege ParkUSA
  2. 2.Department of Computer Science and Institute for Advanced Computer StudiesUniversity of MarylandCollege ParkUSA

Personalised recommendations