Advertisement

Die Logiken von Boole und Büchi-Elgot-Trakhtenbrot in der Beschreibung diskreter Systeme

  • Wolfgang Thomas

Zusammenfassung

Die von Büchi, Elgot und Trakhtenbrot um 1960 eingeführte Logik zur Beschreibung des Verhaltens endlicher Automaten wird in einer intuitiven Darstellung vorgestellt, und zwar als Erweiterung der Booleschen Logik um einen Parameter für diskrete Zeit. Ausgehend von der Charakterisierung der Booleschen Logik durch OBDDs (Ordered Binary Decision Diagrams) wird die Äquivalenz dieser „Büchi-Elgot-Trakhtenbrot-Logik“ mit dem Berechnungsmodell des endlichen Automaten erläutert. Abschließend werden Anwendungen und didaktische Aspekte der Theorie diskreter Systeme diskutiert.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Literatur

  1. [AHU74]
    A.V. Aho, J.E. Hopcroft, J.D. Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley, Reading, Mass. 1974.zbMATHGoogle Scholar
  2. [BK95]
    D. Basin, N. Klarlund, Hardware-verification using monadic second-order logic, in: Computer Aided Verification (P. Wolper, Ed.), Lecture Notes in Computer Science 939, Springer-Verlag, Berlin 1995, pp. 31–41.Google Scholar
  3. [Bo1854]
    G. Boole, An Investigation of the Laws of Thought, Walton and Marberly, London 1854.Google Scholar
  4. [Bry92]
    R. Bryant, Symbolic Boolean manipulation with ordered binary decision diagrams, ACM Computing Surveys 24 (1992), 293–318.CrossRefGoogle Scholar
  5. [Büc60]
    J.R. Büchi, Weak second-order arithmetic and finite automata, Z. Math. Logik Grundl. Math. 6 (1960), 66–92.zbMATHCrossRefGoogle Scholar
  6. [Büc62]
    J.R. Büchi, Mathematische Theorie des Verhaltens endlicher Automaten, Zeitschrift für Angew. Math. und Mechanik 42 (1962), T9–T16.zbMATHCrossRefGoogle Scholar
  7. [BÜEl58]
    J.R. Büchi, C.C. Elgot, Decision problems of weak second order arithmetics and finite automata, Part I, Notices Amer. Math. Soc. 5 (1958), 834.Google Scholar
  8. [Elg61]
    C.C. Elgot, Decision problems of finite automata design and related arithmetics, Trans. Amer. Math. Soc. 98 (1961), 21–51.MathSciNetCrossRefGoogle Scholar
  9. [HU79]
    J.E. Hopcroft, J.D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, Mass. 1979.zbMATHGoogle Scholar
  10. [Kla98]
    N. Klarlund, Mona & Fido: The logic-automaton connection in practice, in: Computer Science Logic (M. Nielsen, W. Thomas, Eds.), Lecture Notes in Computer Science 1414, Springer-Verlag, Berlin 1998, pp. 311–326.Google Scholar
  11. [McM93]
    K. L. McMillan, Symbolic Model Checking, Kluwer Acad. Publ., Boston 1993.zbMATHCrossRefGoogle Scholar
  12. [Mey75]
    A.R. Meyer, Weak monadic second-order theory of successor is not elementary recursive, in: Logic Colloquium, Proc. Symp. on Logic, Boston, 1972 (R. Parikh, Ed.), Lecture Notes in Computer Science 453, Springer-Verlag, Berlin 1975, pp. 132–154.Google Scholar
  13. [MST98]
    O. Matz, N. Schweikardt, W. Thomas, The monadic quantifier alternation hierarchy over grids and graphs, Information and Computation (erscheint).Google Scholar
  14. [Myh57]
    J. Myhill, Finite automata and representation of events, WADC Rep. TR 57-624, Fundamental Concepts in the Theory of Systems, 1957, pp. 112-137.Google Scholar
  15. [RS60]
    M.O. Rabin, D. Scott, Finite automata and their decision problems, IBM J. Research and Development 3 (1959), 114–125.MathSciNetCrossRefGoogle Scholar
  16. [Sto74]
    L.H. Stockmeyer, The Complexity of Decision Problems in Automata Theory and Logic, PhD Thesis, Dep. of Electr. Eng., MIT, Cambridge, Mass. 1974.Google Scholar
  17. [Str94]
    H. Straubing, Finite Automata, Formal Logic, and Circuit Complexity, Birkhäuser, Boston 1994.zbMATHCrossRefGoogle Scholar
  18. [Tho90]
    W. Thomas, Automata on infinite objects, in: Handbook of Theoretical Computer Science, Vol. b (J.v. Leeuwen, Ed.), Elsevier Sci. Publ., Amsterdam 1990, pp. 135–191.Google Scholar
  19. [Tra58]
    B.A. Trakhtenbrot, The synthesis of logical nets whose operators are described in terms of one-place predicate calculus, Dokl. Akad. Nauk SSSR 118 (1958), 646–649 (in Russisch).MathSciNetzbMATHGoogle Scholar
  20. [Tra62]
    B.A. Trakhtenbrot, Finite automata and the logic of one-place predicates, Sib. Math. J. 3 (1962), 103–131 in Russisch). Engl. Transl.: AMS Transl. 59 (1966), 23-55.zbMATHGoogle Scholar

Copyright information

© Friedr. Vieweg & Sohn Verlagsgesellschaft mbH, Braunschweig/Wiesbaden 1999

Authors and Affiliations

  • Wolfgang Thomas
    • 1
  1. 1.Lehrstuhl für Informatik VIIRWTH AachenDeutschland

Personalised recommendations