DROPS

Document

DOI: 10.4230/LIPIcs.CPM.2023.14

MUL-Tree Pruning for Consistency and Compatibility

Authors: Christopher Hampson, Daniel J. Harvey, Costas S. Iliopoulos, Jesper Jansson, Zara Lim, and Wing-Kin Sung

Published in: LIPIcs, Volume 259, 34th Annual Symposium on Combinatorial Pattern Matching (CPM 2023)

Abstract

A multi-labelled tree (or MUL-tree) is a rooted tree leaf-labelled by a set of labels, where each label may appear more than once in the tree. We consider the MUL-tree Set Pruning for Consistency problem (MULSETPC), which takes as input a set of MUL-trees and asks whether there exists a perfect pruning of each MUL-tree that results in a consistent set of single-labelled trees. MULSETPC was proven to be NP-complete by Gascon et al. when the MUL-trees are binary, each leaf label is used at most three times, and the number of MUL-trees is unbounded. To determine the computational complexity of the problem when the number of MUL-trees is constant was left as an open problem. Here, we resolve this question by proving a much stronger result, namely that MULSETPC is NP-complete even when there are only two MUL-trees, every leaf label is used at most twice, and every MUL-tree is either binary or has constant height. Furthermore, we introduce an extension of MULSETPC that we call MULSETPComp, which replaces the notion of consistency with compatibility, and prove that MULSETPComp is NP-complete even when there are only two MUL-trees, every leaf label is used at most thrice, and every MUL-tree has constant height. Finally, we present a polynomial-time algorithm for instances of MULSETPC with a constant number of binary MUL-trees, in the special case where every leaf label occurs exactly once in at least one MUL-tree.

Cite as

Christopher Hampson, Daniel J. Harvey, Costas S. Iliopoulos, Jesper Jansson, Zara Lim, and Wing-Kin Sung. MUL-Tree Pruning for Consistency and Compatibility. In 34th Annual Symposium on Combinatorial Pattern Matching (CPM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 259, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{hampson_et_al:LIPIcs.CPM.2023.14,
  author =	{Hampson, Christopher and Harvey, Daniel J. and Iliopoulos, Costas S. and Jansson, Jesper and Lim, Zara and Sung, Wing-Kin},
  title =	{{MUL-Tree Pruning for Consistency and Compatibility}},
  booktitle =	{34th Annual Symposium on Combinatorial Pattern Matching (CPM 2023)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-276-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{259},
  editor =	{Bulteau, Laurent and Lipt\'{a}k, Zsuzsanna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2023.14},
  URN =		{urn:nbn:de:0030-drops-179682},
  doi =		{10.4230/LIPIcs.CPM.2023.14},
  annote =	{Keywords: multi-labelled tree, phylogenetic tree, consistent, compatible, pruning, algorithm, NP-complete}
}

Document

DOI: 10.4230/LIPIcs.CSL.2013.348

One-variable first-order linear temporal logics with counting

Authors: Christopher Hampson and Agi Kurucz

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various timelines. However, following the introduction of the monodic formulas (where temporal operators can be applied only to subformulas with at most one free variable), there has been a renewed interest in understanding extensions of the one-variable fragment and identifying those that are decidable. Here we analyse the one-variable fragment of temporal logic extended with counting (to two), interpreted in models with constant, decreasing, and expanding first-order domains. We show that over most classes of linear orders these logics are (sometimes highly) undecidable, even without constant and function symbols, and with the sole temporal operator 'eventually'. A more general result says that the bimodal logic of commuting linear and pseudo-equivalence relations is undecidable. The proofs are by reductions of various counter machine problems.

Cite as

Christopher Hampson and Agi Kurucz. One-variable first-order linear temporal logics with counting. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 348-362, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{hampson_et_al:LIPIcs.CSL.2013.348,
  author =	{Hampson, Christopher and Kurucz, Agi},
  title =	{{One-variable first-order linear temporal logics with counting}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{348--362},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.348},
  URN =		{urn:nbn:de:0030-drops-42072},
  doi =		{10.4230/LIPIcs.CSL.2013.348},
  annote =	{Keywords: modal and temporal logic, counting, decision procedures}
}

Search Results

Documents authored by Hampson, Christopher

MUL-Tree Pruning for Consistency and Compatibility

Abstract

Cite as

One-variable first-order linear temporal logics with counting

Abstract

Cite as

Thanks for your feedback!

Could not send message