Document Open Access Logo

Decidability and Complexity of Tree Share Formulas

Authors Xuan Bach Le, Aquinas Hobor, Anthony W. Lin

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.19.pdf
  • Filesize: 0.56 MB
  • 14 pages

Document Identifiers

Author Details

Xuan Bach Le
Aquinas Hobor
Anthony W. Lin

Cite As Get BibTex

Xuan Bach Le, Aquinas Hobor, and Anthony W. Lin. Decidability and Complexity of Tree Share Formulas. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.19

Abstract

Fractional share models are used to reason about how multiple actors share ownership of resources. We examine the decidability and complexity of reasoning over the "tree share" model of Dockins et al. using first-order logic, or fragments thereof. We pinpoint a connection between the basic operations on trees union, intersection, and complement and countable atomless Boolean algebras, allowing us to obtain decidability with the precise complexity of both first-order and existential theories over the tree share model with the aforementioned operations. We establish a connection between the multiplication operation on trees and the theory of word equations, allowing us to derive the decidability of its existential theory and the undecidability of its full first-order theory. We prove that the full first-order theory over the model with both the Boolean operations and the restricted multiplication operation (with constants on the right hand side) is decidable via an embedding to tree-automatic structures.

Subject Classification

Keywords
  • Fractional Share Models
  • Resource Accounting
  • Countable Atomless Boolean Algebras
  • Word Equations
  • Tree Automatic Structures

Metrics

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

References

  1. Parosh Aziz Abdulla, Yu-Fang Chen, Lukás Holík, Richard Mayr, and Tomás Vojnar. When simulation meets antichains. In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, pages 158-174, 2010. URL: http://dx.doi.org/10.1007/978-3-642-12002-2_14.
  2. H. Abdulrab and J.P Pechuchet. Solving word equations. In Journal of Symbolic Computation, pages 499-521, 1989. Google Scholar
  3. Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Program Logics for Certified Compilers. Cambridge University Press, New York, NY, USA, 2014. Google Scholar
  4. Leonard Berman. The complexity of logical theories. Theoretical Computer Science, 11(1):71-77, May 1980. URL: http://dx.doi.org/10.1016/0304-3975(80)90037-7.
  5. A. Blumensath. Automatic Structures. PhD thesis, RWTH Aachen, 1999. Google Scholar
  6. A. Blumensath and E. Grade. Finite presentations of infinite structures: automata and interpretations. In Theory of Computer Systems, pages 641-674, 2004. Google Scholar
  7. John Boyland. Checking interference with fractional permissions. In Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings, pages 55-72, 2003. URL: http://dx.doi.org/10.1007/3-540-44898-5_4.
  8. J Richard Büchi and Steven Senger. Definability in the existential theory of concatenation and undecidable extensions of this theory. In The Collected Works of J. Richard Büchi, pages 671-683. Springer, 1990. 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. Available on: http://www.grappa.univ-lille3.fr/tata, 2007. release October, 12th 2007.
  10. Robert Dockins, Aquinas Hobor, and Andrew W. Appel. A fresh look at separation algebras and share accounting. In Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, pages 161-177, 2009. URL: http://dx.doi.org/10.1007/978-3-642-10672-9_13.
  11. Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic. In 17th European Symposium of Programming (ESOP 2008), pages 353-367, April 2008. URL: http://www.comp.nus.edu.sg/~hobor/publications/concurrent_esop.pdf.
  12. Aquinas Hobor and Cristian Gherghina. Barriers in concurrent separation logic. In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, pages 276-296, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19718-5_15.
  13. Joxan Jaffar. Minimal and complete word unification. J. ACM, 37(1):47-85, 1990. URL: http://dx.doi.org/10.1145/78935.78938.
  14. Sanjay Jain, Bakhadyr Khoussainov, Frank Stephan, Dan Teng, and Siyuan Zou. Semiautomatic structures. In Computer Science - Theory and Applications - 9th International Computer Science Symposium in Russia, CSR 2014, Moscow, Russia, June 7-11, 2014. Proceedings, pages 204-217, 2014. URL: http://dx.doi.org/10.1007/978-3-319-06686-8_16.
  15. Bakhadyr Khoussainov and Mia Minnes. Three lectures on automatic structures. In Logic Colloquium 2007 (F. Delon, U. Kohlenbach, P. Maddy, and F. Stephan, editors), Lecture Notes in Logic, vol. 35, Association for Symbolic Logic, pages 132-176, 2007. Google Scholar
  16. Antoni Koscielski and Leszek Pacholski. Complexity of Makanin’s algorithm. J. ACM, 43(4):670-684, 1996. URL: http://dx.doi.org/10.1145/234533.234543.
  17. Dexter Kozen. Complexity of boolean algebras. In Theoretical Computer Science 10, pages 221-247, 1980. Google Scholar
  18. D. Kuske. Theories of orders on the set of words. In Theoretical Informatics and Applications 40, pages 53-74, 2006. Google Scholar
  19. Xuan Bach Le, Cristian Gherghina, and Aquinas Hobor. Decision procedures over sophisticated fractional permissions. In Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, pages 368-385, 2012. URL: http://dx.doi.org/10.1007/978-3-642-35182-2_26.
  20. G. S Makanin. The problem of solvability of equations in a free semigroup. In Mat. Sbornik, pages 147-236, 1977. Google Scholar
  21. G. S Makanin. Equations in a free group. In Izvestiya AN SSSR, pages 1199-1273, 1982-1983. Google Scholar
  22. G.S Makanin. Decidability of the universal and positive theories of a free group. In Izvestiya AN SSSR, pages 735-749, 1984-1985. Google Scholar
  23. S. Marchenkov. Unsolvability of positive ∀ ∃-theory of free semi-group. In Sibirsky mathmatichesky jurnal, pages 196-198, 1982. Google Scholar
  24. Kim Marriott and Martin Odersky. Negative boolean constraints. In Theoretical Computer Science 160, pages 365-380, 1996. Google Scholar
  25. W. Plandowski. Satisfiability of word equations with constants is in PSPACE. In Journal of the Association for Computing Machinery, pages 483-496, 2004. Google Scholar
  26. W. Plandowski. An efficient algorithm for solving word equations. In Proc 38th Annual Symposium on Theory of Computing, pages 467-476, 2006. Google Scholar
  27. M.O. Rabin. Decidability of second-order theories and automata on infinite trees. In Trans AMS, pages 341-360, 1960. Google Scholar
  28. Stijn Vermeeren. Embeddings into the countable atomless Boolean algebra. 2010. URL: http://stijnvermeeren.be/download/mathematics/embeddings.pdf.
  29. Jules Villard. Heaps and Hops. Ph.D. thesis, Laboratoire Spécification et Vérification, École Normale Supérieure de Cachan, France, February 2011. Google Scholar
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