Thomas Schwentick ; Thomas Zeume - Two-Variable Logic with Two Order Relations

lmcs:715 - Logical Methods in Computer Science, March 2, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:15)2012
Two-Variable Logic with Two Order RelationsArticle

Authors: Thomas Schwentick ; Thomas Zeume

    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.


    Volume: Volume 8, Issue 1
    Published on: March 2, 2012
    Imported on: February 2, 2011
    Keywords: Computer Science - Logic in Computer Science,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Foundations of XML - Safe Processing of Dynamic Data over the Internet; Funder: European Commission; Code: 233599

    9 Documents citing this article

    Consultation statistics

    This page has been seen 1516 times.
    This article's PDF has been downloaded 424 times.