Verification in loosely synchronous queue-connected discrete timed automata

We look at a model of a queue system that consists of the following components:

1. Two discrete timed automata W (the “writer”) and R (“the reader”).

2. One unrestricted queue that can be used to send messages from W to R. There is no bound on the length of the queue.

W and R do not share a global clock and operate in a loosely synchronous way. That is, the absolute value of the difference between the local time of W and the local time of R is always bounded by a positive constant. We show that the binary reachability for these systems is effectively computable, and this result is generalized to the case when there are two queues (one from W to R and the other from R to W) that operate in half-duplex. We then present some properties (e.g., safety, invariance, etc.) that can be verified for loosely synchronous queue-connected discrete timed automata and give an example of a system composed of a sensor and a controller that is verifiable using our results.