Title: Expressive Automata with Counting

Duration: 3 years

Research Area: Knowledge Representation and Engineering

Finite-state automata are one of the most fundamental formalisms in theoretical computer science. They have proven to be a useful tool in many areas, such as formal verification or as a means of proving the decidability of expressive logics applied for knowledge representation. Especially in the areas mentioned, it is desirable to model situations that go beyond regularity. There is a long tradition of adding counting mechanisms to finite automata with the aim of obtaining computational models that are both expressive and maintain decidability of relevant problems. For the word case, there are now a wealth of well-researched models such as pushdown automata, one-counter automata, or Parikh automata. However, for the case of finite and infinite tree-like structures, which are used for describing parallel processes or to encode tree-like models of logical formalisms, it is of interest to better understand the computational properties of expressive tree automation models.

Aims

The aim of the research project is to investigate how tree automata can be enriched by counting mechanisms to test global and local properties of trees. One focus is on models that can be used to show the decidability of expressive logics. An example of this are Parikh tree automata, whose expressiveness corresponds to that of a fragment of Monadic Second-Order Logic with cardinality constrains over (infinite) trees.

Problem

We plan to investigate various tree automata theoretically with counting mechanisms and to classify them in the context of existing results. Typical questions include:

• How does the expressiveness of the different models relate to each other?
• Which closure properties hold?
• Are important problems like emptiness and membership decidable?
• Do logic characterizations exist?

Technology

We use methods and proof techniques that come from different areas of theoretical computer science and expand or adapt them to our setting. These include common automata constructions or reductions of other issues.

Outlook

We believe that the results of this project provide both the theoretical foundations and concrete methods to establish decidability and complexity results for formalisms from various areas of computer science such as knowledge representation or verification.

Publications

• Luisa Herrmann, Vincent Peth, and Sebastian Rudolph. Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Team

Lead

• Prof. Dr. Sebastian Rudolph

Team Members

• Dr. Luisa Herrmann