Monitoring the Full Range of w-RegularProperties of Stochastic Systems

摘要

We present highly accurate deterministic, probabilistic andhybrid methods for monitoring the full range of w-regular properties,specified as Streett automata, of stochastic systems modeled as Hid-den Markov Chains. The deterministic algorithms employ timeouts thatare set dynamically to achieve desired accuracy. The probabilistic algo-rithms employ coin tossing and can give highly accurate monitors whenthe system behavior is not known. The hybrid algorithms combine boththese techniques. The monitoring algorithms have been implemented asa tool. The tool takes a high level description of an application withprobabilities and also a Streett automaton that specifies the propertyto be monitored. It generates a monitor for monitoring computations ofthe application. Experimental results comparing the effectiveness of thedifferent algorithms are presented.