Let them be part of our lives

Current results

We have so far given exact characterizations of when a system is monitorable with respect to a property and is strongly monitorable with respect to a property. For cases when a system is monitorable with respect to a property, we have developed monitoring techniques that can obtain arbitrarily high levels of accuracy close to 1. These techniques were implemented and were shown to be effective using some examples. In order to implement the monitors, we have developed estimation techniques for hybrid systems based on particle filters. Due to its highly nonlinear(the discrete jumping evolution), particle filter shows its advantage in the state estimation. Since the experimental system has several million high-dimensional hybrid states, so by using Rao-Blackwellization, it's possible to reduce the dimension while resampling is performed to get higher accuracy with less particles, also Kalman filters are used for continuous variables for a better performance.

Fig. 1 and Fig. 2 show the state estimation of a sample trajectory of the system we described before. The blue curve is the continuous variable(velocity), and the green curve and black curve are the two discrete variables(representing the states of property automaton which can not be observed directly). Performance of particle filter on hybrid system is good.

Fig. 1   A Sample Trajectory

Fig. 2   State Estimation of the sample trajectory

With decently good state estimation, monitor is running online to get the measures we define: acceptance and rejection accuracies. Below is the chart of the two accuracies after 100 runs with different parameters: timer in property automaton and probability threshold in monitor.


You are here: Home Current results