Complexity analysis of tree share structure

DOI10.1007/978-3-030-02768-1_5zbMATH Open1519.68059OpenAlexW2896259295MaRDI QIDQ6166137FDOQ6166137

Authors Xuan-Bach D. Le, Aquinas Hobor, Anthony Widjaja Lin

Publication date 2 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2010.02340

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are hard to implement due to a lack of a systematic theoretical study. We show that the first-order theory of the full Boolean algebra of tree shares (that is, with all tree-share constants) is decidable and has the same complexity as of the first-order theory of Countable Atomless Boolean Algebras. We prove that combining this additive structure with a constant-restricted unary multiplicative "relativization" operator has a non-elementary lower bound. We examine the consequences of this lower bound and prove that it comes from the combination of both theories by proving an upper bound on a generalization of the restricted multiplicative theory in isolation.

Recommendations

• Decidability and complexity of tree share formulas
• scientific article; zbMATH DE number 7310251
• Rough analysis of computation trees
• Complexity Analysis of Generalized and Fractional Hypertree Decompositions
• Complexity of tree homomorphisms
• Complexity of algorithm and operations on trees
• On the complexity of computing treelength
• On the Complexity of Computing Treelength

Cited in

(1)

• Decidability and complexity of tree share formulas

This page was built for publication: Complexity analysis of tree share structure

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166137)