Control of dense-time Discrete Event Systems using digital-clocks to observe event-occurrence times

We study the supervisory control of dense-time discrete event systems (DESs) where controllers employ finite precision digital-clocks to observe the event occurrence times, relaxing the assumption of the prior works that time can be measured precisely. The passing of time, in our paper, is measured using the number of ticks generated by a digital-clock. We formalize the notion of a control policy that employs observations of events and their occurrence times as measured using a digital-clock for computing the control actions, and show that it can be equivalently represented as a "digitalized"- automaton. We introduce the notion of observability with respect to the partial observation of time resulting from the use of a digital-clock, and show that this together with controllability (for timed setting) serves as a necessary and sufficient condition for the existence of a supervisor to enforce a real-time specification on a dense-time DES. The observability condition presented in the paper is quite different from the one arising due to a partial observation of events for the reason that a partial observation of time is in general nondeterministic.