License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.16
URN: urn:nbn:de:0030-drops-128286
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12828/
Go to the corresponding LIPIcs Volume Portal

Abdulla, Parosh Aziz ; Atig, Mohamed Faouzi ; Dave, Vrunda ; Krishna, Shankara Narayanan

On the Separability Problem of String Constraints

pdf-format:
LIPIcs-CONCUR-2020-16.pdf (2 MB)

Abstract

We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an ExpSpace algorithm for the separability of a useful class of straight-line string constraints, and a Pspace-hardness result.

BibTeX - Entry

@InProceedings{abdulla_et_al:LIPIcs:2020:12828,
  author =	{Parosh Aziz Abdulla and Mohamed Faouzi Atig and Vrunda Dave and Shankara Narayanan Krishna},
  title =	{{On the Separability Problem of String Constraints}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12828},
  URN =		{urn:nbn:de:0030-drops-128286},
  doi =		{10.4230/LIPIcs.CONCUR.2020.16},
  annote =	{Keywords: string constraints, separability, interpolants}
}

Keywords: string constraints, separability, interpolants
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI