Paper: On the Expressiveness and Complexity of Randomization in Finite State Monitors (at LICS 2008)

Authors: Rohit Chadha A. Prasad Sistla Mahesh Viswanathan

Abstract

The continuous run-time monitoring of the behavior of a system is a technique that is used both as a complementary approach to formal verification and testing to ensure reliability, as well as a means to discover emergent properties in a distributed system, like intrusion and event correlation. The monitors in all these scenarios can be abstractly viewed as automata that process a (unbounded) stream of events to and from the component being observed, and raise an ``alarm'' when an error or intrusion is discovered. These monitors indicate the absence of error or intrusion in a behavior implicitly by the absence of an alarm.In this paper we study the power of randomization in run-time monitoring. Specifically, we examine \emph{finite memory} monitoring algorithms that toss coins to make decisions on the behavior they are observing. We give a number of results that characterize, topologically as well as with respect to their computational power, the sets of sequences the monitors permit. We also present results on the complexity of deciding non-emptiness of the set of sequences permitted by a monitor.

BibTeX

  @InProceedings{ChadhaSistlaViswana-OntheExpressiveness,
    author = 	 {Rohit Chadha and A. Prasad Sistla and Mahesh Viswanathan},
    title = 	 {On the Expressiveness and Complexity of Randomization in Finite State Monitors},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {18--29},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }