Document Open Access Logo

Deciding Piecewise Testable Separability for Regular Tree Languages

Authors Jean Goubault-Larrecq, Sylvain Schmitz

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.97.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Author Details

Jean Goubault-Larrecq
Sylvain Schmitz

Cite As Get BibTex

Jean Goubault-Larrecq and Sylvain Schmitz. Deciding Piecewise Testable Separability for Regular Tree Languages. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 97:1-97:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.97

Abstract

The piecewise testable separability problem asks, given two input languages, whether there exists a piecewise testable language that contains the first input language and is disjoint from the second. We prove a general characterisation of piecewise testable separability on languages in a well-quasiorder, in terms of ideals of the ordering. This subsumes the known characterisations in the case of finite words. In the case of finite ranked trees ordered by homeomorphic embedding, we show using effective representations for tree ideals that it entails the decidability of piecewise testable separability when the input languages are regular. A final byproduct is a new proof of the decidability of whether an input regular language of ranked trees is piecewise testable, which was first shown in the unranked case by Bojanczyk, Segoufin, and Straubing [Log. Meth. in Comput. Sci., 8(3:26), 2012].

Subject Classification

Keywords
  • Well-quasi-order
  • ideal
  • tree languages
  • first-order logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, and Bengt Jonsson. Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design, 25(1):39-65, 2004. URL: http://dx.doi.org/10.1023/B:FORM.0000033962.51898.1a.
  2. Jorge Almeida. Some algorithmic problems for pseudovarieties. Publicationes Mathematicae Debrecen, 54(suppl.):531-552, 1999. Google Scholar
  3. Jorge Almeida and Marc Zeitoun. The pseudovariety 𝖩 is hyperdecidable. RAIRO Theoretical Informatics and Applications, 31:457-482, 1997. Google Scholar
  4. Kazuyuki Asada and Naoki Kobayashi. On word and frontier languages of unsafe higher-order grammars. In ICALP 2016, Leibniz International Proceedings in Informatics, 2016. To appear. URL: https://arxiv.org/abs/1604.01595.
  5. Leo Bachmair and David A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Logic and Computation, 1(4):329-349, 1985. URL: http://dx.doi.org/10.1016/S0747-7171(85)80019-5.
  6. Mikołaj Bojańczyk, Luc Segoufin, and Howard Straubing. Piecewise testable tree languages. Logical Methods in Computer Science, 8(3), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(3:26)2012.
  7. Robert Bonnet. On the cardinality of the set of initial intervals of a partially ordered set. In Infinite and finite sets\string: to Paul Erdős on his 60th birthday, Vol. 1, Coll. Math. Soc. János Bolyai, pages 189-198. North-Holland, 1975. Google Scholar
  8. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. In LICS 2016. ACM, 2016. To appear. Google Scholar
  9. H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications. Inria, 2007. URL: http://tata.gforge.inria.fr/.
  10. Bruno Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 44:178-186, 1991. Google Scholar
  11. Wojciech Czerwiński, Wim Martens, and Tomáš Masopust. Efficient separability of regular languages by subsequences and suffixes. In ICALP 2013, volume 7966 of Lecture Notes in Computer Science, pages 150-161. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39212-2_16.
  12. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, and Georg Zetzsche. A characterization for decidable separability by piecewise testable languages. Preprint, 2015. An extended abstract appeared as: W. Czerwiński, W. Martens, L. van Rooijen, and M. Zeitoun. A note on decidable separability by piecewise testable languages. In FCT 2015, volume 9210 of LNCS, pages 173-185. Springer, 2015. URL: http://arxiv.org/abs/1410.1042v2.
  13. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part I: Completions. In STACS 2009, volume 3 of Leibniz International Proceedings in Informatics, pages 433-444. LZI, 2009. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2009.1844.
  14. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Computer Science, 8(3), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(3:28)2012.
  15. Jean Goubault-Larrecq, Prateek Karandikar, K. Narayan Kumar, and Philippe Schnoebelen. The ideal approach to computing closed subsets in well-quasi-orderings. In preparation, 2016. See also an earlier version in: J. Goubault-Larrecq. On a generalization of a result by Valk and Jantzen. Research Report LSV-09-09, LSV, ENS Cachan, 2009. URL: http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf.
  16. Peter Habermehl, Roland Meyer, and Harro Wimmel. The downward-closure of Petri net languages. In ICALP 2010, volume 6199 of Lecture Notes in Computer Science, pages 466-477. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14162-1_39.
  17. Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In POPL 2016, pages 151-163. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837627.
  18. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(2):326-336, 1952. URL: http://dx.doi.org/10.1112/plms/s3-2.1.326.
  19. Pierre Jullien. Contribution à l'étude des types d'ordres dispersés. Thèse de doctorat, Université de Marseille, 1969. Google Scholar
  20. Joseph B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s Conjecture. Transactions of the American Mathematical Society, 95(2):210-225, 1960. URL: http://dx.doi.org/10.2307/1993287.
  21. Ranko Lazić and Sylvain Schmitz. The ideal view on Rackoff’s coverability technique. In RP 2015, volume 9328 of Lecture Notes in Computer Science, pages 1-13. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-24537-9_8.
  22. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In LICS 2015, pages 56-67. IEEE Press, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.16.
  23. Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, and Mooly Sagiv. Decidability of inferring inductive invariants. In POPL 2016, pages 217-231. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837640.
  24. Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. Separating regular languages by piecewise testable and unambiguous languages. In MFCS 2013, volume 8087 of Lecture Notes in Computer Science, pages 729-740. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40313-2_64.
  25. Thomas Place and Marc Zeitoun. Automata column: The tale of the quantifier alternation hierarchy of first-order logic over words. SIGLOG News, 2(3):4-17, 2015. URL: http://dx.doi.org/10.1145/2815493.2815495.
  26. Imre Simon. Piecewise testable events. In Automata Theory and Formal Languages, volume 33 of Lecture Notes in Computer Science, pages 214-222. Springer, 1975. URL: http://dx.doi.org/10.1007/3-540-07407-4_23.
  27. Thomas G. Szymanski and John H. Williams. Noncanonical extensions of bottom-up parsing techniques. SIAM Journal on Computing, 5(2):231-250, 1976. URL: http://dx.doi.org/10.1137/0205019.
  28. W. W. Tait. A counterexample to a conjecture of Scott and Suppes. Journal of Symbolic Logic, 24(1):15-16, 1959. URL: http://dx.doi.org/10.2307/2964569.
  29. Jan van Leeuwen. Effective constructions in well-partially-ordered free monoids. Discrete Mathematics, 21(3):237-252, 1978. URL: http://dx.doi.org/10.1016/0012-365X(78)90156-5.
  30. Georg Zetzsche. An approach to computing downward closures. In ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 440-451. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_35.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact