2009 | OriginalPaper | Buchkapitel
Monitoring the Full Range of ω-Regular Properties of Stochastic Systems
verfasst von : Kalpana Gondi, Yogeshkumar Patel, A. Prasad Sistla
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
We present highly accurate deterministic, probabilistic and hybrid methods for monitoring the full range of
ω
-regular properties, specified as Streett automata, of stochastic systems modeled as Hidden Markov Chains. The deterministic algorithms employ timeouts that are set dynamically to achieve desired accuracy. The probabilistic algorithms employ coin tossing and can give highly accurate monitors when the system behavior is not known. The hybrid algorithms combine both these techniques. The monitoring algorithms have been implemented as a tool. The tool takes a high level description of an application with probabilities and also a Streett automaton that specifies the property to be monitored. It generates a monitor for monitoring computations of the application. Experimental results comparing the effectiveness of the different algorithms are presented.