2014 | OriginalPaper | Buchkapitel
Probabilistic Automata for Safety LTL Specifications
verfasst von : Dileep Kini, Mahesh Viswanathan
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.