Can reduce the mfotl formula to a normal temporal logic with some constraints w.r.t. time stamps. Keep a separate data structures for monitoring all the timed events. If an expected future event does not happen in the given time bound, then report violation of property.
Can reduce the mfotl formula to a normal temporal logic with some constraints w.r.t. time stamps. Keep a separate data structures for monitoring all the timed events. If an expected future event does not happen in the given time bound, then report violation of property.