Use of a metric in supervisory control of probabilistic discrete event systems

This work represents a natural extension of our work on optimal probabilistic supervisory control of probabilistic discrete event systems (PDESs). In that work, a pseudometric on the initial states of two probabilistic generators that represent probabilistic systems is used to measure the distance between the two systems. The pseudometric is given a fixed point characterization. This paper gives a logical characterization of the same pseudometric such that the distance between two systems is measured by a formula that distinguishes between the systems the most. A trace characterization of the pseudometric is then derived from the logical characterization. Further, the solution of the problem of approximation of a given probabilistic generator with another generator of a prespecified structure is suggested such that the new model is as close as possible to the original one in the pseudometric. The significance of the approximation is then discussed.