Automata constructions for logical properties play an important role in the formal analysis of the system both statically and dynamically. In this paper, we present constructions of finite-state probabilistic monitors (FPM) for safety properties expressed in LTL. FPMs are probabilistic automata on infinite words that have a special, absorbing reject state, and given a cut-point λ ∈ [0, 1], accept all words whose probability of reaching the reject state is at most 1 ? λ. We consider Safe-LTL, the collection of LTL formulas built using conjunction, disjunction, next, and release operators, and show that (a) for any formula Φ, there is an FPM with cut-point 1 of exponential size that recognizes the models of Φ, and (b) there is a family of Safe-LTL formulas, such that the smallest FPM with cut-point 0 for this family is of doubly exponential size. Next, we consider the fragment LTL(G) of Safe-LTL wherein always operator is used instead of release operator and show that for any formula Φ ∈ LTL(G) (c) there is an FPM with cut-point 0 of exponential size for Φ, and (d) there is a robust FPM of exponential size for Φ, where a robust FPM is one in which the acceptance probability of any word is bounded away from the cut-point.We also show that these constructions are optimal.
展开▼
