The MSO plus U Theory of (N, <) Is Undecidable

被引：8
作者：
Bojanczyk, Mikolaj [1 ]
Parys, Pawel [1 ]
Torunczyk, Szymon [1 ]
机构：
[1] Univ Warsaw, Ul Banacha 2, PL-02097 Warsaw, Poland
来源：
33RD SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2016) | 2016年 / 47卷
关键词：
automata; logic; unbounding quantifier; bounds; undecidability; WEAK MSO;
D O I：
10.4230/LIPIcs.STACS.2016.21
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We consider the logic mso+u, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N, <=) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.
引用
收藏
页数：8
相关论文
共 14 条
[1]  
[Anonymous], 2012, IARCS ANN C FDN SOFT
[2]  
Blumensath A, 2014, LECT NOTES COMPUT SC, V8634, P87, DOI 10.1007/978-3-662-44522-8_8
[3]  
Bojanczyk M, 2004, LECT NOTES COMPUT SC, V3210, P41
[4]   Bounds in ω-regularity [J].
Bojanczyk, Mikolaj ;
Colcombet, Thomas .
21ST ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2006, :285-+
[5]   Weak MSO plus U over infinite trees [J].
Bojanczyk, Mikolaj ;
Torunczyk, Szymon .
29TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE, (STACS 2012), 2012, 14 :648-660
[6]  
Bojanczyk M, 2014, LECT NOTES COMPUT SC, V8573, P50
[7]  
Bojanczyk M, 2014, LECT NOTES COMPUT SC, V8573, P38
[8]   Weak MSO with the Unbounding Quantifier [J].
Bojanczyk, Mikolaj .
THEORY OF COMPUTING SYSTEMS, 2011, 48 (03) :554-576
[9]  
Brazdil Tomas, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P23, DOI 10.1007/978-3-642-31424-7_8
[10]  
Carapelle Claudia, 2013, CONCUR 2013 - Concurrency Theory. 24th International Conference, CONCUR 2013. Proceedings: LNCS 8052, P455, DOI 10.1007/978-3-642-40184-8_32
12