Algorithms, Theory & Logic

Research Spotlight: From Newton to Turing to cyber-physical systems

February 2018
In 1937, a young Englishman by the name of Alan M. Turing published a paper with the obscure title "On computable numbers, with an application to the Entscheidungsproblem'' in the Proceedings of the London Mathematical Society. In doing so, he arguably laid the mathematical foundations of modern computer science. Turing's seminal contribution was to show that the famous Entscheidungsproblem, formulated by the great German mathematician David Hilbert several years earlier, could not be solved: more precisely, Turing proved (in modern parlance) that the problem of determining whether a given computer program halts could not be done algorithmically---in other words that the famous Halting Problem is undecidable.

Although seemingly at the time a rather esoteric concern, the Halting Problem (and related questions) have dramatically gained in importance and relevance in more contemporary times. Fast forward to the 21st Century: nowadays, it is widely acknowledged that enabling engineers, programmers, and researchers to automatically verify and certify the correctness of the computer systems that they design is one of the Grand Challenges of computer science. In increasingly many instances, it is absolutely critical that the software governing various aspects of our daily lives (such as that running on an aircraft controller, for example) behave exactly as intended, lest catastrophic consequences ensue.

What classes of infinite-state programs can be analyzed algorithmically?

Researchers at the Foundations of Algorithmic Verification group are investigating what classes of infinite-state programs can, at least in principle, be fully handled and analyzed algorithmically by viewing computer programs abstractly as dynamical systems, and they seek to design exact algorithms enabling one to fully analyse the behaviour of such systems. In particular, they are presently tackling a range of central algorithmic problems from verification, synthesis, performance, and control for linear dynamical systems, drawing among others on tools from number theory, Diophantine geometry, and algebraic geometry, with the overarching goal of offering a systematic exact computational treatment of various important classes of dynamical systems and other fundamental models used in mathematics, computer science, and the quantitative sciences. Some of their achievements include several decidability and hardness results for linear recurrence sequences, which can be used to model simple loops in computer programs, answering a number of longstanding open questions in the mathematics and computer science literature.

In a series of recent papers [1, 2],  they have attacked the so-called Zero Problem for linear differential equations, i.e., the question of determining algorithmically whether the unique solution to a given linear differential equation has a zero or not. Such equations, which go back as far as Newton, are ubiquitous in mathematics, physics, and engineering; they are also particularly useful to model cyber-physical systems, i.e., digital systems that evolve in and interact with a continuous environment. In their work, they obtained several important partial results: if one is interested in the existence of a zero over a bounded time interval, then it is possible to determine this algorithmically, provided that a certain hypothesis from the mathematical field of number theory, known as Schanuel's Conjecture, is true. They were also able to partially account for the fact that the Zero Problem has hitherto remained open in full generality: indeed, if one were able to solve it in dimension 9 (or higher), then in turn this would enable one to solve various longstanding hard open problems from a field of mathematics known as Diophantine approximation. In doing so, they therefore exhibited surprising and unexpected connections between the modelling and analysis of cyber-physical systems and seemingly completely unrelated deep mathematical theories dealing with questions about whole numbers.


[1] Ventsislav Chonev, Joel Ouaknine, and James Worrell. On recurrent reachability for continuous linear dynamical systems. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016.

[2] Ventsislav Chonev, Joel Ouaknine, and James Worrell. On the Skolem Problem for continuous linear dynamical systems. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP), 2016.

Amaury Pouly wins Ackermann Award

June 2017
Amaury Pouly, a postdoc in Joël Oukanine's Foundations of Automatic Verification Group, has received the 2017 Ackermann Award for his PhD thesis, “Continuous-time computation models: From computability to computational complexity.” The Ackermann Award is an international prize presented annually to the author of an exceptional doctoral dissertation in the field of Computer Science Logic.

Amaury Pouly's thesis shows that problems which can be solved with a computer in a reasonable amount of time (more specifically problems which belong to the class P of the famous open problem “P = NP?”) can be characterized as polynomial length solutions of polynomial differential equations. This result paves the way for reformulating certain questions and concepts of theoretical computer science in terms of ordinary polynomial differential equations. It also revisits analog computational models and demonstrates that analog and digital computers actually have the same computing power, both in terms of what they can calculate (computability) and what they can solve in reasonable (polynomial) time.

Advanced Automata Theory Course at TU Kaiserslautern

April 2017
Rupak Majumdar and Daniel Neider are co-teaching Advanced Automata Theory at the University of Kaiserslautern in the Summer 2017 semester.

The course meets Tuesdays 08:15-09:45 in room 48-210 and Wednesdays 13:45-15:15 in room 46-280 on the University of Kaiserslautern campus.

Complexity Theory Course at TU Kaiserslautern

November 2016
Rupak Majumdar is teaching Complexity Theory at the University of Kaiserslautern in the Winter 2016-17 semester.

The course meets Mondays 15:30-17:00 at 46-280 and Wednesdays 13:45-15:15 at 46-268.

More information about the course

Three MPI-SWS papers accepted to POPL'17

October 2016
Three papers from MPI-SWS were accepted to ACM POPL 2017:
  • A promising semantics for relaxed-memory concurrency
  • Relational cost analysis
  • Thread modularity at many levels: a pearl in compositional verification

Rupak Majumdar will chair CAV 2017

October 2016
Rupak Majumdar and Viktor Kuncak (EPFL) are co-chairs of the 29th International Conference on Computer-Aided Verification (CAV 2017), to be held between July 22 and 28, 2017 in Heidelberg, Germany.

CAV 2017 is the 29th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis and synthesis methods for hardware and software systems. The CAV home page has more information.

Joel Ouaknine will chair LICS 2017

October 2016
Joel Ouaknine is the Program Chair of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), to be held between 20 and 23 June, 2017 in Reykjavik. The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed.