SubsidieMeestersLogic and Automata over Sequences with Data
The project aims to overcome undecidability in automata theory over infinite alphabets by developing new decidable models and algorithms for analyzing data languages, with applications in graph databases, program verification, and machine learning.
Projectdetails
Introduction
Formal language theory is indisputably one of the most successful theories in theoretical computer science, with many applications in such fields as formal verification, programming languages, and databases, to name a few. Despite this, the standard restriction to finite alphabets has been a limiting factor in the applicability of the theory in various important application domains, wherein sequences with data (i.e., ranging over an infinite domain like the set of integers and the set of strings) naturally arise.
Motivation
This has motivated an extensive study of automata over infinite alphabets in the last three decades, which aims to develop algorithms for analyzing data languages. It was, however, quickly realized that permitting anything but the simplest data reasoning results in undecidability for the most fundamental models in the theory. Given the growing practical needs for tools for reasoning about sequences with data, it is crucial that we break through this undecidability barrier.
Project Aim
The aim of the project is to overcome the current undecidability barrier in extending automata theory over infinite alphabets with complex data reasoning.
Objectives
The first concrete objective is, thus, to identify new decidable logic/automata models for data languages that permit complex data reasoning over various data domains, including:
- Integer linear arithmetic
- Real-closed fields
- String constraints
Additionally, the project aims to develop efficient algorithms for analyzing these models.
Contributions
In addition to making fundamental theoretical contributions in automata theory over infinite alphabets, I also aim to address the current practical needs for tools for reasoning about sequences.
Application Domains
Thus, the second objective of the project is to transfer new algorithmic insights to the following important application domains:
- Querying graph databases
- Verification of list-manipulating programs
- Interpretable machine learning for sequences
Financiële details & Tijdlijn
Financiële details
| Subsidiebedrag | € 1.998.956 |
| Totale projectbegroting | € 1.998.956 |
Tijdlijn
| Startdatum | 1-8-2023 |
| Einddatum | 31-7-2028 |
| Subsidiejaar | 2023 |
Partners & Locaties
Projectpartners
- RHEINLAND-PFALZISCHE TECHNISCHE UNIVERSITATpenvoerder
Land(en)
Vergelijkbare projecten binnen European Research Council
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
Finite-state abstractions of infinite-state systemsThis project aims to develop methods for abstracting infinite-state systems using finite-state overapproximations to enhance software verification, particularly in concurrent settings. | ERC Starting... | € 1.482.500 | 2023 | Details |
Automata, Dynamics and ActionsThis project aims to solve key problems in group theory and dynamics using finite state automata to develop algorithms and explore their interactions, ultimately proving decidability in various contexts. | ERC Advanced... | € 2.419.896 | 2023 | Details |
Algebraic Formula Lower Bounds and ApplicationsThis project aims to establish lower bounds for algebraic formulas and improve Polynomial Identity Testing algorithms by leveraging structural and algebraic techniques in theoretical computer science. | ERC Consolid... | € 1.869.055 | 2024 | Details |
Coming to Terms: Proof Theory Extended to Definite Descriptions and other TermsExtenDD integrates proof theory and complex terms by developing formal theories of definite descriptions and enhancing sequent calculus, impacting automated deduction and philosophy of language. | ERC Advanced... | € 1.629.775 | 2022 | Details |
Logics and Algorithms for a Unified Theory of HyperpropertiesThis project aims to develop a unified theory and formal tools for hyperproperties in software, focusing on societal values like privacy and fairness, to enhance program verification and synthesis. | ERC Advanced... | € 2.227.500 | 2022 | Details |
Finite-state abstractions of infinite-state systems
This project aims to develop methods for abstracting infinite-state systems using finite-state overapproximations to enhance software verification, particularly in concurrent settings.
Automata, Dynamics and Actions
This project aims to solve key problems in group theory and dynamics using finite state automata to develop algorithms and explore their interactions, ultimately proving decidability in various contexts.
Algebraic Formula Lower Bounds and Applications
This project aims to establish lower bounds for algebraic formulas and improve Polynomial Identity Testing algorithms by leveraging structural and algebraic techniques in theoretical computer science.
Coming to Terms: Proof Theory Extended to Definite Descriptions and other Terms
ExtenDD integrates proof theory and complex terms by developing formal theories of definite descriptions and enhancing sequent calculus, impacting automated deduction and philosophy of language.
Logics and Algorithms for a Unified Theory of Hyperproperties
This project aims to develop a unified theory and formal tools for hyperproperties in software, focusing on societal values like privacy and fairness, to enhance program verification and synthesis.
Vergelijkbare projecten uit andere regelingen
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
Inzet van computational linguistics voor het vergaren van military intelligenceDit project onderzoekt de haalbaarheid van computational linguistics voor het vergaren van militaire inlichtingen ter verbetering van veiligheid. | Mkb-innovati... | € 20.000 | 2023 | Details |
Inzet van computational linguistics voor het vergaren van military intelligence
Dit project onderzoekt de haalbaarheid van computational linguistics voor het vergaren van militaire inlichtingen ter verbetering van veiligheid.