DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2016.19

Decidability and Complexity of Tree Share Formulas

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

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.FSTTCS.2016.19,
  author =	{Le, Xuan Bach and Hobor, Aquinas and Lin, Anthony W.},
  title =	{{Decidability and Complexity of Tree Share Formulas}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{19:1--19:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.19},
  URN =		{urn:nbn:de:0030-drops-68544},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.19},
  annote =	{Keywords: Fractional Share Models, Resource Accounting, Countable Atomless Boolean Algebras, Word Equations, Tree Automatic Structures}
}

Document

DOI: 10.4230/DagSemProc.10351.3

A Theory of Termination via Indirection

Authors: Robert Dockins and Aquinas Hobor

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract

Step-indexed models provide approximations to a class of domain equations and can prove type safety, partial correctness, and program equivalence; however, a common misconception is that they are inapplicable to liveness problems. We disprove this by applying step-indexing to develop the first Hoare logic of total correctness for a language with function pointers and semantic assertions. In fact, from a liveness perspective, our logic is stronger: we verify explicit time resource bounds. We apply our logic to examples containing nontrivial "higher-order" uses of function pointers and we prove soundness with respect to a standard operational semantics. Our core technique is very compact and may be applicable to other liveness problems. Our results are machine checked in Coq.

Cite as

Robert Dockins and Aquinas Hobor. A Theory of Termination via Indirection. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dockins_et_al:DagSemProc.10351.3,
  author =	{Dockins, Robert and Hobor, Aquinas},
  title =	{{A Theory of Termination via Indirection}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.3},
  URN =		{urn:nbn:de:0030-drops-28050},
  doi =		{10.4230/DagSemProc.10351.3},
  annote =	{Keywords: Step-indexed Models, Termination}
}

Search Results

Documents authored by Hobor, Aquinas

Decidability and Complexity of Tree Share Formulas

Abstract

Cite as

A Theory of Termination via Indirection

Abstract

Cite as

Thanks for your feedback!

Could not send message