Document

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

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.

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

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

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.

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} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail