Document Open Access Logo

Semiring Provenance for Fixed-Point Logic

Authors Katrin M. Dannert, Erich Grädel, Matthias Naaf, Val Tannen

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.17.pdf
  • Filesize: 0.56 MB
  • 22 pages

Document Identifiers

Author Details

Katrin M. Dannert
  • RWTH Aachen University, Germany
Erich Grädel
  • RWTH Aachen University, Germany
Matthias Naaf
  • RWTH Aachen University, Germany
Val Tannen
  • University of Pennsylvania, Philadelphia, PA, USA

Cite AsGet BibTex

Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen. Semiring Provenance for Fixed-Point Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.17

Abstract

Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • Finite Model Theory
  • Semiring Provenance
  • Absorptive Semirings
  • Fixed-Point Logics

Metrics

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

Related Versions

  • Due to space reasons, a number of technical details and proofs have been omitted. They are available in the full version of this paper at https://arxiv.org/abs/1910.07910.

References

  1. Y. Amsterdamer, D. Deutch, and V. Tannen. On the limitations of provenance for queries with difference. In 3rd Workshop on the Theory and Practice of Provenance, TaPP'11, 2011. See also CoRR abs/1105.2255. Google Scholar
  2. K. Apt and E. Grädel, editors. Lectures in Game Theory for Computer Scientists. Cambridge University Press, 2011. URL: https://doi.org/10.1017/CBO9780511973468.
  3. K. Dannert and E. Grädel. Provenance analysis: A perspective for description logics? In C. Lutz et al., editor, Description Logic, Theory Combination, and All That, Lecture Notes in Computer Science Nr. 11560. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-22102-7_12.
  4. K. Dannert and E. Grädel. Semiring provenance for guarded logics. In Hajnal Andréka and István Németi on Unity of Science: From Computing to Relativity Theory through Algebraic Logic, Outstanding Contributions to Logic. Springer, 2021. Google Scholar
  5. K. Dannert, E. Grädel, M. Naaf, and V. Tannen. Generalized absorptive polynomials and provenance semantics for fixed-point logic. arXiv: 1910.07910 [cs.LO], 2019. URL: https://arxiv.org/abs/1910.07910.
  6. D. Deutch, T. Milo, S. Roy, and V. Tannen. Circuits for datalog provenance. In Proc. 17th International Conference on Database Theory ICDT, pages 201-212. OpenProceedings.org, 2014. URL: https://doi.org/10.5441/002/icdt.2014.22.
  7. M. Droste and P. Gastin. Weighted automata and weighted logics. In Handbook of weighted automata, pages 175-211. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-01492-5_5.
  8. M. Droste, W. Kuich, and H. Vogler, editors. Handbook of Weighted Automata. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-01492-5.
  9. M. Droste and G. Rahonis. Weighted automata and weighted logics on infinite words. In International Conference on Developments in Language Theory, pages 49-58. Springer, 2006. URL: https://doi.org/10.1007/11779148_6.
  10. F. Geerts and A. Poggi. On database query languages for K-relations. J. Applied Logic, 8(2):173-185, 2010. URL: https://doi.org/10.1016/j.jal.2009.09.001.
  11. F. Geerts, T. Unger, G. Karvounarakis, I. Fundulaki, and V. Christophides. Algebraic structures for capturing the provenance of SPARQL queries. J. ACM, 63(1):7:1-7:63, 2016. URL: https://doi.org/10.1145/2810037.
  12. E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema, and S. Weinstein. Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2007. URL: https://doi.org/10.1007/3-540-68804-8.
  13. E. Grädel and V. Tannen. Semiring provenance for first-order model checking. arXiv:1712.01980 [cs.LO], 2017. URL: https://arxiv.org/abs/1712.01980.
  14. E. Grädel and V. Tannen. Provenance analysis for logic and games. Moscow Journal of Combinatorics and Number Theory, 9(3):203-228, 2020. URL: https://doi.org/10.2140/moscow.2020.9.203.
  15. T. Green, Z. Ives, and V. Tannen. Reconcilable differences. In Database Theory - ICDT 2009, pages 212-224, 2009. URL: https://doi.org/10.1145/1514894.1514920.
  16. T. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Principles of Database Systems PODS, pages 31-40, 2007. URL: https://doi.org/10.1145/1265530.1265535.
  17. T. Green and V. Tannen. The semiring framework for database provenance. In Proceedings of PODS, pages 93-99. ACM, 2017. URL: https://doi.org/10.1145/3034786.3056125.
  18. A. Lluch-Lafuente and U. Montanari. Quantitative mu-calculus and CTL defined over constraint semirings. Theoretical Compututer Science, 346(1):135-160, 2005. URL: https://doi.org/10.1016/j.tcs.2005.08.006.
  19. G. Markowsky. Chain-complete posets and directed sets with applications. Algebra universalis, 6(1):53-68, 1976. Google Scholar
  20. Y. Moschovakis. Elementary induction on abstract structures. North Holland, 1974. Google Scholar
  21. Y. Ramusat, S. Maniu, and P. Senellart. Semiring provenance over graph databases. In 10th USENIX Workshop on the Theory and Practice of Provenance (TaPP 2018), London, 2018. Google Scholar
  22. P. Senellart. Provenance and probabilities in relational databases: From theory to practice. SIGMOD Record, 46(4):5-15, 2017. URL: https://doi.org/10.1145/3186549.3186551.
  23. J. Xu, W. Zhang, A. Alawini, and V. Tannen. Provenance analysis for missing answers and integrity repairs. IEEE Data Eng. Bull., 41(1):39-50, 2018. 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 Imprint Privacy Contact