Document Open Access Logo

Uniformly Automatic Classes of Finite Structures

Author Faried Abu Zaid

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.10.pdf
  • Filesize: 0.6 MB
  • 21 pages

Document Identifiers

Author Details

Faried Abu Zaid
  • Camelot Management Consultants, CoE Artificial Intellegence for Information Management, Munich, Germany

Funding

  • Abu Zaid, Faried: The presented work was conducted while the author was affiliated with the Technische Universität Ilmenau.

Cite As Get BibTex

Faried Abu Zaid. Uniformly Automatic Classes of Finite Structures. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2018.10

Abstract

We investigate the recently introduced concept of uniformly tree-automatic classes in the realm of parameterized complexity theory. Roughly speaking, a class of finite structures is uniformly tree-automatic if it can be presented by a set of finite trees and a tuple of automata. A tree t encodes a structure and an element of this structure is encoded by a labeling of t. The automata are used to present the relations of the structure. We use this formalism to obtain algorithmic meta-theorems for first-order logic and in some cases also monadic second-order logic on classes of finite Boolean algebras, finite groups, and graphs of bounded tree-depth. Our main concern is the efficiency of this approach with respect to the hidden parameter dependence (size of the formula). We develop a method to analyze the complexity of uniformly tree-automatic presentations, which allows us to give upper bounds for the runtime of the automata-based model checking algorithm on the presented class. It turns out that the parameter dependence is elementary for all the above mentioned classes. Additionally we show that one can lift the FPT results, which are obtained by our method, from a class C to the closure of C under direct products with only a singly exponential blow-up in the parameter dependence.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Theory of computation → Fixed parameter tractability
  • Theory of computation → Formal languages and automata theory
Keywords
  • Automatic Structures
  • Model Checking
  • Fixed-Parameter Tractability
  • Algorithmic Meta Theorems

Metrics

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

References

  1. Faried Abu Zaid, Erich Grädel, and Frederic Reinhardt. Advice Automatic Structures and Uniformly Automatic Classes. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), 2017. URL: http://www.logic.rwth-aachen.de/pub/abuzaid/AbuGraRei17.pdf.
  2. Simone Bova and Barnaby Martin. First-Order Queries on Finite Abelian Groups. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), volume 41 of Leibniz International Proceedings in Informatics (LIPIcs), pages 41-59, Dagstuhl, Germany, 2015. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2015.41.
  3. Thomas Colcombet and Christof Löding. Transforming structures by set interpretations. CoRR, abs/cs/0703039, 2007. URL: http://arxiv.org/abs/cs/0703039.
  4. B. Courcelle, J. A. Makowsky, and U. Rotics. Linear Time Solvable Optimization Problems on Graphs of Bounded Clique-Width. Theory Comput. Systems, 33(2):125-150, April 2000. URL: http://dx.doi.org/10.1007/s002249910009.
  5. Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation, 85(1):12-75, March 1990. URL: http://dx.doi.org/10.1016/0890-5401(90)90043-H.
  6. Antoine Durand-Gasselin and Peter Habermehl. Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree. In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of LIPIcs, pages 242-253. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2012.242.
  7. Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49(2):129-141, 1961. URL: https://eudml.org/doc/213582.
  8. Jochen Eisinger. Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract). In Michael Kaminski and Simone Martini, editors, Computer Science Logic, number 5213 in Lecture Notes in Computer Science, pages 431-445. Springer Berlin Heidelberg, September 2008. DOI: 10.1007/978-3-540-87531-4_31. URL: http://link.springer.com/chapter/10.1007/978-3-540-87531-4_31.
  9. Jeanne Ferrante and Charles W. Rackoff. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer Berlin Heidelberg, 1979. URL: http://link.springer.com/10.1007/BFb0062837.
  10. JÖRG Flum, ERICH Grädel, and THOMAS Wolke, editors. Logic and Automata: History and Perspectives. Amsterdam University Press, 2008. URL: http://www.jstor.org/stable/j.ctt46mv83.
  11. Roland Fraïssé. Sur l'extension aux relations de quelques propriétés des ordres. Annales scientifiques de l'École Normale Supérieure, 71(4):363-388, 1954. URL: https://eudml.org/doc/81696.
  12. M. Frick and M. Grohe. The complexity of first-order and monadic second-order logic revisited. In 17th Annual IEEE Symposium on Logic in Computer Science, 2002. Proceedings, pages 215-224, 2002. URL: http://dx.doi.org/10.1109/LICS.2002.1029830.
  13. Jakub Gajarsky and Petr Hlineny. Faster Deciding MSO Properties of Trees of Fixed Height, and Some Consequences. In Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), volume 18 of Leibniz International Proceedings in Informatics (LIPIcs), pages 112-123, Dagstuhl, Germany, 2012. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2012.112.
  14. Martin Grohe. Logic, Graphs, and Algorithms. Electronic Colloquium on Computational Complexity (ECCC), 14(091), 2007. URL: http://eccc.hpi-web.de/eccc-reports/2007/TR07-091/index.html.
  15. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding First-order Properties of Nowhere Dense Graphs. In Proceedings of the 46th Annual ACM Symposium on Theory of Computing, STOC '14, pages 89-98, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2591796.2591851.
  16. Thomas W. Hungerford. Algebra, volume 73 of Graduate Texts in Mathematics. Springer New York, New York, NY, 1980. URL: http://link.springer.com/10.1007/978-1-4612-6101-8.
  17. Neeraj Kayal and Timur Nezhmetdinov. Factoring Groups Efficiently. In International Colloquium on Automata, Languages and Programming (ICALP), volume 5555 of Lecture Notes in Computer Science. Springer Verlag, 2009. URL: http://research.microsoft.com/apps/pubs/default.aspx?id=102435.
  18. Felix Klaedtke. Ehrenfeucht–Fraïssé goes automatic for real addition. Information and Computation, 208(11):1283-1295, November 2010. URL: http://dx.doi.org/10.1016/j.ic.2010.07.003.
  19. Dietrich Kuske and Markus Lohrey. Automatic structures of bounded degree revisited. J. Symbolic Logic, 76(4):1352-1380, December 2011. URL: http://dx.doi.org/10.2178/jsl/1318338854.
  20. Alexander Langer, Felix Reidl, Peter Rossmanith, and Somnath Sikdar. Evaluation of an MSO-Solver. In David A. Bader and Petra Mutzel, editors, ALENEX, pages 55-63. SIAM / Omnipress, 2012. URL: http://dblp.uni-trier.de/db/conf/alenex/alenex2012.html#LangerRRS12.
  21. Derek C. Oppen. A 2^2^2^pn upper bound on the complexity of Presburger Arithmetic. Journal of Computer and System Sciences, 16(3):323-332, June 1978. URL: http://dx.doi.org/10.1016/0022-0000(78)90021-1.
  22. Felix Reidl, Peter Rossmanith, Fernando Sánchez Villaamil, and Somnath Sikdar. A Faster Parameterized Algorithm for Treedepth. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming, number 8572 in Lecture Notes in Computer Science, pages 931-942. Springer Berlin Heidelberg, July 2014. DOI: 10.1007/978-3-662-43948-7_77. URL: http://link.springer.com/chapter/10.1007/978-3-662-43948-7_77.
  23. Detlef Seese. Linear Time Computable Problems and First-Order Descriptions. Mathematical Structures in Computer Science, 6(6):505-526, 1996. 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