On the expressiveness and complexity of randomization in finite state monitors

ABSTRACT

In this article, we introduce the model of finite state probabilistic monitors (FPM), which are finite state automata on infinite strings that have probabilistic transitions and an absorbing reject state. FPMs are a natural automata model that can be seen as either randomized run-time monitoring algorithms or as models of open, probabilistic reactive systems that can fail. We give a number of results that characterize, topologically as well as with respect to their computational power, the sets of languages recognized by FPMs. We also study the emptiness and universality problems for such automata and give exact complexity bounds for these problems.

REFERENCES

• 1: Alpern, B., and Schneider, F. 1985. Defining liveness. Inf. Proc. Lett. 21, 181--185.
• 2: Amorium, M., and Rosu, G. 2005. Efficient monitoring of omega-languages. In Proceedings of the International Conference on Computer Aided Verification'. Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, Berlin, 364--378.
• 3: Baier, C., Bertrand, N., and Größer, M. 2008. On decision problems for probabilistic Büchi automata. In Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany (FoSSaCS). 287--301.
• 4: Christel Baier , Marcus Grosser, Recognizing ?-regular Languages with Probabilistic Automata, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.137-146, June 26-29, 2005 [doi>10.1109/LICS.2005.41]
• 5: Bauer, A., Leucker, M., and Schallhart, C. 2006. Monitoring of real-time properties. In Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science. Springer-Verlag, Berlin, Germany, 260--272.
• 6: Rohit Chadha , A. Prasad Sistla , Mahesh Viswanthan, On the Expressiveness and Complexity of Randomization in Finite State Monitors, Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science, p.18-29, June 24-27, 2008 [doi>10.1109/LICS.2008.42]
• 7: Feng Chen , Grigore Roşu, Mop: an efficient and generic runtime verification framework, Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 8: A. Condon , R. J. Lipton, On the complexity of space bounded interactive proofs, Proceedings of the 30th Annual Symposium on Foundations of Computer Science, p.462-467, October 30-November 01, 1989 [doi>10.1109/SFCS.1989.63519]
• 9: Michel Diaz , Guy Juanole , Jean-Pierre Courtiat, Observer-A Concept for Formal On-Line Validation of Distributed Systems, IEEE Transactions on Software Engineering, v.20 n.12, p.900-913, December 1994 [doi>10.1109/32.368136]
• 10: Rusins Freivalds, Probabilistic Two-Way Machines, Proceedings on Mathematical Foundations of Computer Science, p.33-45, August 31-September 04, 1981
• 11: Gates, A., and Roach, S. 2001. Dynamics: Comprehensive support for runtime monitoring. In Runtime Verification. ENTCS. Elsevier Publishing, Amsterdam, The Netherlands.
• 12: Kalpana Gondi , Yogeshkumar Patel , A. Prasad Sistla, Monitoring the Full Range of ω-Regular Properties of Stochastic Systems, Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, December 18-20, 2008, Savannah, GA [doi>10.1007/978-3-540-93900-9_12]
• 13: Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Computability classes for enforcement mechanisms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.175-205, January 2006 [doi>10.1145/1111596.1111601]
• 14: Havelund, K., and Rosu, G. 2001. Monitoring java programs with JavaPathExplorer. In Runtime Verification. ENTCS. Elsevier Publishing, Amesterdam, The Netherlands.
• 15: Neil Immerman, Nondeterministic space is closed under complementation, SIAM Journal on Computing, v.17 n.5, p.935-938, October 1988 [doi>10.1137/0217058]
• 16: Clinton Jeffery , Wenyi Zhou , Kevin Templer , Michael Brazell, A lightweight architecture for program execution monitoring, Proceedings of the 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.67-74, June 16-16, 1998, Montreal, Quebec, Canada
• 17: Kemeny, J., and Snell, J. 1976. Denumerable Markov Chains. Springer-Verlag, Berlin, Germany.
• 18: Kim, M., Viswanathan, M., B.-Abdullah, H., Kannan, S., Lee, I., and Sokolsky, O. 1999. Formally specified monitoring of temporal properties. In Proceedings of the IEEE Euromicro Conference on Real-time Systems. IEEE Computer Society Press, Los Alamitos, 114--122.
• 19: Kortenkamp, D., Milam, T., Simmons, R., and Fernandez, J. L. 2001. Collecting and analyzing data from distributed control programs. In Runtime Verification. ENTCS. Elsevier Publishing, Amesterdam, The Netherlands.
• 20: M. W. Alford , J. P. Ansart , G. Hommel , L. Lamport , B. Liskov , G. P. Mullery , F. B. Schneider, Distributed systems: methods and tools for specification. An advanced course, Springer-Verlag New York, Inc., New York, NY, 1985
• 21: Jarred Adam Ligatti , David P. Walker, Policy enforcement via program monitoring, Princeton University, Princeton, NJ, 2006
• 22: Ligatti, J., Bauer, L., and Walker, D. 2005. Edit automata: Enforcement mechanisms for runtime security policies. Int. J. Inf. Sec. 4, 1--2 (Feb.), 2--16.
• 23: Jay Ligatti , Lujo Bauer , David Walker, Run-Time Enforcement of Nonsafety Policies, ACM Transactions on Information and System Security (TISSEC), v.12 n.3, p.1-41, January 2009 [doi>10.1145/1455526.1455532]
• 24: Mansouri-Samani, M., and Sloman, M. 1992. Monitoring distributed systems: A survey. Res. Rep. DOC92/93, Imperial College, London, UK.
• 25: Tiziana Margaria , A. Prasad Sistla , Bernhard Steffen , Lenore D. Zuck, Taming interface specifications, CONCUR 2005 - Concurrency Theory, Springer-Verlag, London, 2005 [doi>10.1007/11539452_41]
• 26: Nasu, M., and Honda, N. 1968. Fuzzy events realized by finite probabilistic automata. Inf. Cont. 12, 4, 284--303.
• 27: Papoulis, A., and Pillai, S. U. 2002. Probability, Random Variables and Stochastic Processes. McGraw Hill, New York.
• 28: Vern Paxson, Automated packet trace analysis of TCP implementations, ACM SIGCOMM Computer Communication Review, v.27 n.4, p.167-179, Oct. 1997
• 29: Azaria Paz, Introduction to probabilistic automata (Computer science and applied mathematics), Academic Press, Inc., Orlando, FL, 1971
• 30: Perrin, D., and Pin, J.-E. 2004. Infinite Words: Automata, Semigroups, Logic and Games. Elseiver, Amesterdam, The Netherlands.
• 31: B. Plattner , J. Nievergelt, Special Feature: Monitoring Program Execution: A Survey, Computer, v.14 n.11, p.76-93, November 1981 [doi>10.1109/C-M.1981.220255]
• 32: Pnueli, A., and Zaks, A. 2006. PSL model checking and runtime verification via testers. In Proceedings of the 14th International Symposium on Formal Methods. Springer-Verlag, Berlin Germany, 573--586.
• 33: Rabin, M. O. 1963. Probabilitic automata. Inf. Cont. 6, 3, 230--245.
• 34: Marcus J. Ranum , Kent Landfield , Michael T. Stolarchuk , Mark Sienkiewicz , Andrew Lambeth , Eric Wall, Implementing a Generalized Tool for Network Monitoring, Proceedings of the 11th Conference on Systems Administration, p.1-8, October 26-31, 1997
• 35: Arto Salomaa, Formal languages, Academic Press Professional, Inc., San Diego, CA, 1987
• 36: Sammapun, U., Lee, I., Sokolsky, O., and Regehr, J. 2007. Statistical runtime checking of probabilistic properties. In Proceedings of the 7th International Workshop on Runtime Verification. Springer-Verlag, Berlin, Germany, 164--175.
• 37: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 38: Beth A. Schroeder, On-Line Monitoring: A Tutorial, Computer, v.28 n.6, p.72-78, June 1995 [doi>10.1109/2.386988]
• 39: A. P. Sistla, On characterization of safety and liveness properties in temporal logic, Proceedings of the fourth annual ACM symposium on Principles of distributed computing, p.39-48, August 1985, Minaki, Ontario, Canada [doi>10.1145/323596.323600]
• 40: Sistla, A. P., and Srinivas, A. R. 2008. Monitoring temporal properties of stochastic systems. In Proceedings of International Conference on Verification, Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4905. Springer-Verlag, Berlin, Germany, 294--308.
• 41: Szelepcsenyi, R. 1987. The method of forcing for nondeterministic automata. Bull. EATCS 33, 96--100.
• 42: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 43: Time Rover. 1997. http://www.time-rover.com.
• 44: Moshe Y. Vardi, Automatic verification of probabilistic concurrent finite state programs, Proceedings of the 26th Annual Symposium on Foundations of Computer Science, p.327-338, October 21-23, 1985 [doi>10.1109/SFCS.1985.12]
• 45: Mahesh Viswanathan , Sampath Kannan , Insup Lee, Foundations for the run-time analysis of software systems, University of Pennsylvania, Philadelphia, PA, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
      F.1.2 Modes of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

General Terms:
Languages, Security, Theory, Verification

Keywords:
Omega automata, probabilistic automata, randomization, runtime verification, topology