Weak alternating automata in Isabelle/HOL

被引：0
作者：
Merz, S [1 ]
机构：
[1] Univ Munich, Inst Informat, D-8000 Munich, Germany
来源：
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS | 2000年 / 1869卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：424 / 441
页数：18
相关论文
共 12 条
  • [1] [Anonymous], HDB THEORETICAL COMP
  • [2] BUCHI JR, 1992, INT C LOG METH PHIL, P1
  • [3] KUPFERMAN O, 1997, 5 ISR S THEOR COMP S, P147
  • [4] MULLER D, 1988, 3 IEEE S LOG COMP SC, P422
  • [5] MULLER DE, 1986, LECT NOTES COMPUT SC, V226, P275
  • [6] Safra S., 1988, 29th Annual Symposium on Foundations of Computer Science (IEEE Cat. No.88CH2652-6), P319, DOI 10.1109/SFCS.1988.21948
  • [7] Schneider K, 1999, LECT NOTES COMPUT SC, V1690, P255
  • [8] THOMAS W, 2000, JEWELS FOREVER CONTR, P109
  • [9] Thomas W., 1997, HDB FORMAL LANGUAGES, VIII, P389, DOI DOI 10.1007/978-3-642-59126-6
  • [10] Vardi M. Y., 1987, Proceedings of the Symposium on Logic in Computer Science (Cat. No.87CH2464-6), P167
12