I found that one of the problems at International Mathematic Olympic 2016 is really interesting. One can consider and solve that problem using Model Checking techniques in Computer Science.
Problem
There are \(n \geq 2\) line segments in the plane such that every two segments cross, and no three segments meet at a point. Geoff has to choose an endpoint of each segment and place a frog on it, facing the other endpoint. Then he will clap his hands \(n - 1\) times. Every time he claps, each frog will immediately jump forward to the next intersection point on its segment. Fogs never change the direction of their jumps. Geoff wishes to place the frogs in such a way that no two of them will ever occupy the same intersection point at the same time.
- Prove that Geoff can always fulfill his wish if \(n\) is odd.
- Prove that Geoff can never fulfill his wish if \(n\) is even.
Discussion
I will not talk about the proof in mathematics. You can think about it. Here I would like to relate this problem to the race problem in multi-threaded programming. As a result, it will come to the dead-lock problem in software engineering.
For example, can we use model checking technique to verify these property?