It was a sweltering summer morning in July 2016, and the olive grove close to the town of Andria in the Italian countryside baked silently in the 40-degree heat. But what began as a quiet morning would soon descend into chaos.
Just past 11am, two passenger trains — both travelling at speeds of over 100 kilometres per hour — zipped through the grove. They were heading in opposite directions, with only a single train track between them. Neither driver saw the other coming as they approached a bend in the tracks. Witnesses recall hearing a deafening bang as the two trains collided head-on. Crumpled carriages, mangled metal, and twisted bodies laid strewn across the parched earth between the dry olive trees. Twenty-three people died that day and more than 50 were injured, making the accident one of Italy’s worst train disasters to date.
Across Europe and elsewhere in the world, engineers work hard to avoid accidents such as this. There are now control systems that track train positions, calculate braking distances, and adjust traffic signals accordingly, thereby ensuring trains are always kept a safe distance apart. Autopilots and air traffic control systems work on similar notions; and beyond transportation, finance networks, medical and life-support equipment, and even nuclear power plants operate on such safety-check computerised systems.
So how do we know these systems are safe, especially when the consequences are critical, and failure can mean the difference between life and death? System engineers and computer scientists frequently use a method called model checking to verify that the system in question will behave as it’s meant to. Model checking employs mathematical logic, and includes the notion of parity games.
The power of prediction
Parity games provide a useful theoretical framework for model checking and verification as they help distil a complex problem into fairly simple one. Solve a parity game and you can solve a model-checking problem.
In essence, a parity game is played by two players who take turns moving a token along a game board, or graph, comprising of nodes. Each node has a number value assigned to it, and players move from one node to another on each turn. Over the course of a game, nodes can be visited an infinite number of times. One player is assigned to be the “odd” player, while the other is designated as the “even” player. A player wins when the largest value of all of the nodes visited infinitely often is of his designation — in other words, if the largest value of a node visited is odd, then the “odd” player wins the game.
“So the question is, given such a graph and all the values, can we figure out who wins?” says Professor Sanjay Jain from the National University of Singapore (NUS) School of Computing’s Department of Computer Science.
“The goal is for a computing programme to figure out who wins before they even start playing,” says Professor Frank Stephan who holds a joint appointment with NUS’s Department of Computer Science and the Department of Mathematics (Faculty of Science).
Figuring out the winner prior to the game being played is how parity games are used in model checking. “It’s a kind of satisfiability testing,” says Jain, “where you have some constraints, and you want to see if given those constraints, whether a problem can be solved.”
Take the train traffic control system, for example. If you know you have two trains along a 200-kilometre long stretch of track, which are both travelling at speeds of 120 kilometres per hour, what is the minimum safe braking distance required to prevent a collision? Applying model checking with the help of parity games can help answer that question.
Time is of the essence
A key to applying parity games to such problem solving, says Jain, is to be able to do it in the shortest time possible. “It’s useful to solve them fast,” he says.
For many years, the best algorithms mathematicians could come up with for the time required to solve parity games was exponential time. In other words, the time required is of the form of k^n , where k is a constant and n is the size of the problem. In the case of parity games, n would be the number of nodes in the graph.
“Many have tried for 20 to 30 years…and n to the square root n was the best that they could do,” says Stephan. “But it’s important that the time which you need to solve a parity game is not too big.”
And so Stephan, Jain and their collaborators puzzled over the problem. Then in late 2016, they came upon an idea: Why not use quasipolynomial time — n to the power of log n — to solve the problem? In general, quasipolynomials are much smaller numbers compared to exponential numbers. Then in late 2016, they had an idea for a quasipolynomial time algorithm to solve the problem. After trying out various versions over two months, they managed to get their method to work. Quasipolynomial time is much faster than the slightly subexponential time algorithms which were previously used.
The researchers tested the algorithm and found, to their delight, that it worked. “The technique used is different from what most people use — most didn’t expect that this problem of parity games would be solvable significantly faster than the subexponential algorithm of Jurdzinski, Paterson and Zwick,” says Jain, referring to earlier work published that was previously regarded as the quickest way to solve parity games — that is, before Jain and his collaborators turned to quasipolynomial time.
“We showed that the computing time has been reduced quite a bit,” says Jain.
The team from NUS, including Dr. Li Wei from NUS’ Department of Mathematics, and their collaborators from the University of Auckland, Professors Cristian S. Claude and Bakhadyr Khoussainov, wrote a paper on their findings, which they presented at last year’s Symposium on Theory of Computing (STOC) in Montreal, Canada. Their work was awarded Best Paper of the conference, and the team is currently working on getting it published in a journal.
Since then, other groups have tried to improve on their quasipolynomial algorithm. But no one has succeeded in significantly shortening the time it takes. However, improvements have been made to the computing space required. “You can’t create more space because you can’t expand memory so easily, but you can say, ‘Ok, I’ll wait for a longer time,’” says Jain.
The next challenge in the parity games problem, Jain and Stephan agree, is to reduce the time required to solve them even further. “It’s still open whether we can do it in polynomial time,” explains Jain. Polynomial time involves n to the power of a constant, rather than n to the power of log n, which is the case for quasipolynomial time.
“Quasipolynomial time is much longer, so if you can solve it in polynomial time, then the algorithm is so much more desirable,” says Stephan. “You always want fast algorithms.”
