文章基本信息

标题：Two-Variable Logic with Two Order Relations
本地全文：下载
作者：Thomas Schwentick ; Thomas Zeume
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2012
卷号：8
期号：1
页码：1
DOI：10.2168/LMCS-8(1:15)2012
出版社：Technical University of Braunschweig
摘要：It is shown that the finite satisfiability problem for two-variable logic over structures with one total preorder relation, its induced successor relation, one linear order relation and some further unary relations is EXPSPACE-complete. Actually, EXPSPACE-completeness already holds for structures that do not include the induced successor relation. As a special case, the EXPSPACE upper bound applies to two-variable logic over structures with two linear orders. A further consequence is that satisfiability of two-variable logic over data words with a linear order on positions and a linear order and successor relation on the data is decidable in EXPSPACE. As a complementing result, it is shown that over structures with two total preorder relations as well as over structures with one total preorder and two linear order relations, the finite satisfiability problem for two-variable logic is undecidable.
其他关键词：two-variable logic, linear orders, data word