Separating Regular Languages with First-Order Logic
Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in orde...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2016-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1628/pdf |
| _version_ | 1797268638191845376 |
|---|---|
| author | Thomas Place Marc Zeitoun |
| author_facet | Thomas Place Marc Zeitoun |
| author_sort | Thomas Place |
| collection | DOAJ |
| description | Given two languages, a separator is a third language that contains the first
one and is disjoint from the second one. We investigate the following decision
problem: given two regular input languages of finite words, decide whether
there exists a first-order definable separator. We prove that in order to
answer this question, sufficient information can be extracted from semigroups
recognizing the input languages, using a fixpoint computation. This yields an
EXPTIME algorithm for checking first-order separability. Moreover, the
correctness proof of this algorithm yields a stronger result, namely a
description of a possible separator. Finally, we generalize this technique to
answer the same question for regular languages of infinite words. |
| first_indexed | 2024-04-25T01:35:39Z |
| format | Article |
| id | doaj.art-827627c592e84546b09f610536c62e2a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:39Z |
| publishDate | 2016-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-827627c592e84546b09f610536c62e2a2024-03-08T09:43:02ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742016-03-01Volume 12, Issue 110.2168/LMCS-12(1:5)20161628Separating Regular Languages with First-Order LogicThomas PlaceMarc ZeitounGiven two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking first-order separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we generalize this technique to answer the same question for regular languages of infinite words.https://lmcs.episciences.org/1628/pdfcomputer science - formal languages and automata theorycomputer science - logic in computer science |
| spellingShingle | Thomas Place Marc Zeitoun Separating Regular Languages with First-Order Logic Logical Methods in Computer Science computer science - formal languages and automata theory computer science - logic in computer science |
| title | Separating Regular Languages with First-Order Logic |
| title_full | Separating Regular Languages with First-Order Logic |
| title_fullStr | Separating Regular Languages with First-Order Logic |
| title_full_unstemmed | Separating Regular Languages with First-Order Logic |
| title_short | Separating Regular Languages with First-Order Logic |
| title_sort | separating regular languages with first order logic |
| topic | computer science - formal languages and automata theory computer science - logic in computer science |
| url | https://lmcs.episciences.org/1628/pdf |
| work_keys_str_mv | AT thomasplace separatingregularlanguageswithfirstorderlogic AT marczeitoun separatingregularlanguageswithfirstorderlogic |