We aim to model the problem of networked control. Sometimes (e.g., signals at a train junction, a rover on Mars), the systems are operated remotely, but the communication channels may be unreliable. We wish to ensure the specification satisfiability under unreliable channels. To this end, we consider the following game on graphs:
The vertices have no ownership, but the two players player at alternate timesteps. The system has a LTL specification to satisfy on the infinite words generated by the plays. The system player plays remotely and has to send a signal to make a move on the graph. However, the signal could be delayed (with a bound) or lost during the transmission, and the token does not move. Then the environment player makes a move to move the token.
Questions:
- Does the system have a strategy (with/without memory) to satisfy the specification?
- If not, identify the minimal set of unsafe edges that should be removed from the graph so that even if the delays and losses occur, the environment may not take an action such that the specification satisfaction becomes impossible.