Weak Alternating Automata in Isabelle/HOL

Stephan Merz

Abstract

Thomas has presented a novel proof of the closure of omega-regular languages under complementation, using weak alternating automata. This note describes a formalization of this proof in the theorem prover Isabelle/HOL. As an application we have developed a certified translation procedure for PTL formulas to weak alternating automata inside the theorem prover.

© Springer-Verlag

Available as:  gzip'ed Postscript

Reference

@INPROCEEDINGS{merz:weak-alternating,
  title      = "Weak Alternating Automata in {I}sabelle/{HOL}",
  author     = "Stephan Merz",
  editor     = "J. Harrison and M. Aagaard",
  booktitle  = "Theorem Proving in Higher Order Logics:
                13th Intl. Conf., TPHOLs 2000",
  series     = "Lecture Notes in Computer Science",
  volume     = 1869,
  year       = 2000,
  publisher  = "Springer-Verlag",
  pages      = "423--440"
}