Deciding FO-definability of Regular Languages

Agi Kurucz; Vladislav Ryzhikov; Yury Savateev; Michael Zakharyaschev

doi:10.1007/978-3-030-88701-8_15

Deciding FO-definability of Regular Languages

Agi Kurucz, Vladislav Ryzhikov, Yury Savateev, Michael Zakharyaschev

Research output: Contribution to conference › Paper › peer-review

Abstract

We prove that, similarly to known PSPACE-completeness of recognising FO(<)-definability of the language L(A) of a DFA (A), deciding both FO(<,≡)- and FO(<,MOD)-definability (corresponding to circuit complexity in AC^0 and ACC^0) are PSPACE-complete. We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by ‘localisable’ properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSPACE-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for 2NFAs.

Original language	English
Pages	241-257
DOIs	https://doi.org/10.1007/978-3-030-88701-8_15
Publication status	Published - 22 Oct 2021
Event	19th International Conference on Relational and Algebraic Methods in Computer Science - Marseilles, France Duration: 2 Nov 2021 → 5 Nov 2021 Conference number: 19 https://ramics19.lis-lab.fr/

Conference

Conference	19th International Conference on Relational and Algebraic Methods in Computer Science
Abbreviated title	RAMICS 2021
Country/Territory	France
City	Marseilles
Period	2/11/21 → 5/11/21
Internet address	https://ramics19.lis-lab.fr/

Access to Document

10.1007/978-3-030-88701-8_15

Cite this

@conference{c1189df31c464eab8e9664b1e780534d,

title = "Deciding FO-definability of Regular Languages",

abstract = "We prove that, similarly to known PSPACE-completeness of recognising FO(<)-definability of the language L(A) of a DFA (A), deciding both FO(<,≡)- and FO(<,MOD)-definability (corresponding to circuit complexity in AC^0 and ACC^0) are PSPACE-complete. We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by {\textquoteleft}localisable{\textquoteright} properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSPACE-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for 2NFAs.",

author = "Agi Kurucz and Vladislav Ryzhikov and Yury Savateev and Michael Zakharyaschev",

year = "2021",

month = oct,

day = "22",

doi = "10.1007/978-3-030-88701-8_15",

language = "English",

pages = "241--257",

note = "19th International Conference on<br/>Relational and Algebraic Methods in Computer Science, RAMICS 2021 ; Conference date: 02-11-2021 Through 05-11-2021",

url = "https://ramics19.lis-lab.fr/",

}

TY - CONF

T1 - Deciding FO-definability of Regular Languages

AU - Kurucz, Agi

AU - Ryzhikov, Vladislav

AU - Savateev, Yury

AU - Zakharyaschev, Michael

N1 - Conference code: 19

PY - 2021/10/22

Y1 - 2021/10/22

N2 - We prove that, similarly to known PSPACE-completeness of recognising FO(<)-definability of the language L(A) of a DFA (A), deciding both FO(<,≡)- and FO(<,MOD)-definability (corresponding to circuit complexity in AC^0 and ACC^0) are PSPACE-complete. We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by ‘localisable’ properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSPACE-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for 2NFAs.

AB - We prove that, similarly to known PSPACE-completeness of recognising FO(<)-definability of the language L(A) of a DFA (A), deciding both FO(<,≡)- and FO(<,MOD)-definability (corresponding to circuit complexity in AC^0 and ACC^0) are PSPACE-complete. We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by ‘localisable’ properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSPACE-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for 2NFAs.

U2 - 10.1007/978-3-030-88701-8_15

DO - 10.1007/978-3-030-88701-8_15

M3 - Paper

SP - 241

EP - 257

T2 - 19th International Conference on<br/>Relational and Algebraic Methods in Computer Science

Y2 - 2 November 2021 through 5 November 2021

ER -

Deciding FO-definability of Regular Languages

Abstract

Conference

Access to Document

Fingerprint

Cite this