How can a programmer ensure a critical piece of software is bug-free? Theoretical computer scientists use a fundamental question called the reachability problem, which determines whether a computer will reach or avoid various dangerous states when running a program. To better understand the complexity of the problem, researchers turned to a mathematical tool called vector addition systems. In a series of recent breakthroughs, computer scientists have now determined that the complexity of the reachability problem for vector addition systems is defined by a famous function called the Ackermann function, which becomes extremely complex even with small inputs.
----------
Read the full article for links to papers: https://www.quantamagazine.org/an-eas...

CORRECTION: March 13, 2024
Around the same time as Czerwiński and Orlikowski's 2021 paper that raised the lower bound to Leroux and Schmitz’s Ackermann upper bound, Leroux obtained an equivalent result, working independently. Both papers proved the same lower bound and the teams coordinated to publish the papers at the same time. Links to their work can be found here:
- The Reachability Problem for Petri Nets is Not Primitive Recursive, Leroux https://ieeexplore.ieee.org/document/...
- Reachability in Vector Addition Systems is Ackermann-complete, Czerwiński and Orlikowski https://ieeexplore.ieee.org/document/...

----------
Chapters:
00:00 How formal verification finds programming bugs
00:59 The Reachability Problem
01:41 Origins of concurrent computing and resultant challenges
02:40 Vector addition systems (vass) and the reachability problem
04:16 Searching for the complexity of the problem, what's the fastest algorithm?
04:38 Identification of lower and upper bounds of the reachability problem
06:18 The Ackermann function explained
07:32 A final solution to the vasa reachability problem is found

----------
- VISIT our website: https://www.quantamagazine.org
- LIKE us on Facebook:   / quantanews  
- FOLLOW us Twitter:   / quantamagazine  

Quanta Magazine is an editorially independent publication supported by the Simons Foundation: https://www.simonsfoundation.org/