Unifying the Time-Event Spectrum for Stream Runtime Verification

We study the spectra of time-event and of synchronous-asynchronous models of computation for runtime verification, in particular in the context of stream runtime verification (SRV). Most runtime verification formalisms do not involve a notion of time, either by having inputs at all instants (like LTL or Lola) or by reacting to external events in an event-driven fashion (like MOP). Other formalisms consider notions of real-time, ranging from the collection and periodic processing of events to complex computations of the times at which events exist or are produced (like TeSSLa or Striver). Also, some monitoring languages assume that all inputs and outputs change values at once (synchronous), while others allow changes independently (asynchronous).