EXPONENTIAL GAPS IN OUR KNOWLEDGE

被引:0
作者
Aceto, Luca [1 ,2 ]
Kupferman, Orna [3 ]
机构
[1] Aalborg Univ, BRICS, Dept Comp Sci, DK-9220 Aalborg O, Denmark
[2] Reykjavik Univ, Sch Sci & Engn, Dept Comp Sci, IS-103 Reykjavik, Iceland
[3] Hebrew Univ Jerusalem, Sch Engn & Comp Sci, IL-91904 Jerusalem, Israel
来源
BULLETIN OF THE EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE | 2007年 / 92期
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Automata on infinite objects were the key to the solution of several fundamental decision problems in mathematics and logic. Today, automata on infinite objects are used for formal specification and verification of reactive systems. The practical importance of automata in formal methods has motivated a re-examination of the complexity of problems and constructions involving automata. For most problems and constructions, the situation is satisfying, in the sense that even if there is a gap between the upper and the lower bound, it is small. For some fundamental and highly practical cases, however, the gap between the upper and the lower bound is exponential or even larger. The article surveys several such frustrating cases, studies features that they share, and describes recent efforts (with partial success) to close the gaps.
引用
收藏
页码:44 / 64
页数:21
相关论文
共 57 条
  • [1] DEFINING LIVENESS
    ALPERN, B
    SCHNEIDER, FB
    [J]. INFORMATION PROCESSING LETTERS, 1985, 21 (04) : 181 - 185
  • [2] Aminof B, 2006, LECT NOTES COMPUT SC, V4218, P125
  • [3] Armoni R., 2002, LNCS, V2280, P196
  • [4] Beer I, 2001, LECT NOTES COMPUT SC, V2102, P363
  • [5] Boyer R.S., 1983, 35 I COMP SCI COMP A
  • [6] SYMBOLIC MODEL CHECKING - 1020 STATES AND BEYOND
    BURCH, JR
    CLARKE, EM
    MCMILLAN, KL
    DILL, DL
    HWANG, LJ
    [J]. INFORMATION AND COMPUTATION, 1992, 98 (02) : 142 - 170
  • [7] Bounded model checking using satisfiability solving
    Clarke, E
    Biere, A
    Raimi, R
    Zhu, Y
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (01) : 7 - 34
  • [8] Clarke EM, 1999, MODEL CHECKING, P1
  • [9] Courcoubetis C., 1992, Formal Methods in System Design, V1, P275, DOI 10.1007/BF00121128
  • [10] Emerson E. A., 1988, 29th Annual Symposium on Foundations of Computer Science (IEEE Cat. No.88CH2652-6), P328, DOI 10.1109/SFCS.1988.21949