So-called ‘discrete dynamical systems’ form the basis for key computational challenges in a variety of fields, from program analysis and computer-aided verification to artificial intelligence and theoretical biology. Creating algorithmic solutions to make these systems amenable to automated verification techniques remains a major challenge. Researchers at the Max Planck Institute for Software Systems in Saarbrücken and the French ‘Centre National de la Recherche Scientifique’ are now working on advancing this automated verification approach with substantial funding by the European Research Council. ...
So-called ‘discrete dynamical systems’ form the basis for key computational challenges in a variety of fields, from program analysis and computer-aided verification to artificial intelligence and theoretical biology. Creating algorithmic solutions to make these systems amenable to automated verification techniques remains a major challenge. Researchers at the Max Planck Institute for Software Systems in Saarbrücken and the French ‘Centre National de la Recherche Scientifique’ are now working on advancing this automated verification approach with substantial funding by the European Research Council.
The interdisciplinary project, titled ‘Dynamical and Arithmetical Model Checking (DynAMiCs)’, is led by the three principal investigators—Professor Joël Ouaknine, Scientific Director at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken; Professor Florian Luca, also MPI-SWS and Stellenbosch University in South Africa; and Professor Valérie Berthé from the French ‘Institut de recherche en informatique fondamentale’ at the ‘Centre National de la Recherche Scientifique (CNRS)’ at the University Paris Cité.
“The paradigm of ‘model checking’ is a powerful method that allows us to automatically verify, with mathematical certainty, whether a system behaves as intended” says Prof. Joël Ouaknine. However, many discrete dynamical systems—systems that change over time following specific rules—cannot currently be verified with the available model-checking approaches.
One of the leading objectives of this new research project is thus to substantially broaden the classes of dynamical systems and properties that can be algorithmically handled via model checking. Specifically, it aims to tackle longstanding mathematical challenges, such as the Skolem Problem, that could lead to breakthroughs in understanding and verifying the behavior of other complex systems.
The Skolem Problem asks if, within a system following specific mathematical rules, a certain state will eventually be reached. Translated to other instances, this question could ask if a computer program will terminate under specific conditions, when an electric vehicle’s battery will fully deplete following a specific driving pattern, or if a manufacturing robot will reach a precise target after following programmed movements. Although seemingly simple, this mathematical problem has remained unsolved and has puzzled mathematicians and computer scientists alike for nearly a century.
Besides the Skolem Problem, the project also addresses additional longstanding mathematical challenges such as the Pisot Conjecture, piecewise-affine map reachability, and the Periodicity Conjecture. Addressing these complex problems demands innovative approaches that integrate insights from multiple areas of mathematics and computer science. “This funding allows us to leverage the interdisciplinary synergies between different fields, bringing together expertise that might not otherwise have come together,” says Florian Luca. The DynAMiCs project unites expertise in algorithmic verification led by Prof. Joël Ouaknine, symbolic dynamics under Prof. Valérie Berthé, and analytic number theory led by Prof. Florian Luca.
The project is funded via a European Research Council (ERC) Synergy Grant totaling 7.5 million euros over six years, with 5 million euros allocated to MPI-SWS. ERC Grants are among the most prestigious research awards globally, with Synergy Grants being especially competitive and offering the highest funding levels. In the current funding round, 548 proposals were submitted, of which only 57 were approved (10.4%).
Further Information:
Press Release by the European Research Council:
https://erc.europa.eu/news-events/news/erc-2024-synergy-grants-results
List of Selected Projects:
https://erc.europa.eu/sites/default/files/2024-11/erc-2024-syg-results-all-domains.pdf
Scientific Contact:
Professor Joël Ouaknine, PhD
Scientific Director at MPI SWS and Coordinating Principal Investigator of
DynAMiCs
Max Planck Institute for Software Systems, Saarbrücken
Tel: +49 (0)681 9303 9701
E-Mail:
joel@mpi-sws.org
Editor:
Philipp Zapf-Schramm
Max Planck Institute for Informatics
Tel: +49 681 9325 5409
E-Mail:
pzs@mpi-inf.mpg.de
