Rohit Chadha
Skip Abstract Section
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.
- Alpern, B., and Schneider, F. 1985. Defining liveness. Inf. Proc. Lett. 21, 181--185.Google Scholar
Cross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Baier, C. and Größer, M. 2005. Recognizing ω-regular languages with probabilistic automata. In Proceedings of the IEEE Symposium on Login in Computer Science. IEEE Computer Society Press, Los Alamitos, 137--146. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Chadha, R., Sistla, A. P., and Viswanathan, M. 2008. On the expressiveness and complexity of randomization in finite state monitors. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008). IEEE Computer Society Press, Los Alamitos, 18--29. Google ScholarDigital Library
- Chen, F., and Rosu, G. 2007. MOP: An efficient and generic runtime verification framework. In Proceedings of the ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. ACM, New York, 569--588. Google ScholarDigital Library
- Condon, A., and Lipton, R. J. 1989. On the complexity of space bounded interactive proofs (extended abstract). In Proceedings of the 30th Annual Symposium on Foundations of Computer Science. IEEE Computer Society, Press Los Alamitos, 462--467. Google ScholarDigital Library
- Diaz, M., Juanole, G., and Courtiat, J. P. 1994. Observer: A concept for formal on-line validation of distributed systems. IEEE Trans. Softw. Eng. 20, 12, 900--913. Google ScholarDigital Library
- Freivalds, R. 1981. Probabilistic two-way machines. In Proceeding of the Mathematical Foundations of Computer Science. Springer-Verlag, Berlin, Germany, 33--45. Google ScholarDigital Library
- Gates, A., and Roach, S. 2001. Dynamics: Comprehensive support for runtime monitoring. In Runtime Verification. ENTCS. Elsevier Publishing, Amsterdam, The Netherlands.Google Scholar
- Gondi, K., Patel, Y., and Sistla, A. P. 2009. Monitoring the full range of omega-regular properties of stochastic systems. In Proceedings of International Conference on Verification, Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 5403. Springer-Verlag, Berlin, Germany, 105--119. Google ScholarDigital Library
- Hamlen, K. W., Morrisett, G., and Schneider, F. 2006. Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst. 28, 1, 175--205. Google ScholarDigital Library
- Havelund, K., and Rosu, G. 2001. Monitoring java programs with JavaPathExplorer. In Runtime Verification. ENTCS. Elsevier Publishing, Amesterdam, The Netherlands.Google Scholar
- Immerman, N. 1988. Nondeterministic space is closed under complementation. SIAM J. Comput. 17, 935--938. Google ScholarDigital Library
- Jeffery, C., Zhou, W., Templer, K., and Brazell, M. 1998. A lightweight architechture for program execution monitoring. In Proceedings of the ACM Workshop on Program Analysis for Software Tools and Engineering. ACM, New York, 67--74. Google ScholarDigital Library
- Kemeny, J., and Snell, J. 1976. Denumerable Markov Chains. Springer-Verlag, Berlin, Germany.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Lamport, L. 1985. Logical foundation, distributed systems: Methods and tools for specification. Lecture Notes in Computer Science, vol. 190. Springer-Verlag, Berlin, Germany. Google ScholarDigital Library
- Ligatti, J. 2006. Policy enforcement via program monitoring. Ph.D. dissertation, Princeton Univ., Princeton. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- Ligatti, J., Bauer, L., and Walker, D. 2009. Runtime enforcement of nonsafety policy. ACM Trans. Inf. Syst. Sec. 12, 3, 1--41. Google ScholarDigital Library
- Mansouri-Samani, M., and Sloman, M. 1992. Monitoring distributed systems: A survey. Res. Rep. DOC92/93, Imperial College, London, UK.Google Scholar
- Margaria, T., Sistla, A. P., Steffen, B., and Zuck, L. D. 2005. Taming interface specifications. In Proceedings of 16th International Conference on Concurrency Theory (CONCUR). Springer-Verlag, Berlin, Germany, 548--561. Google ScholarDigital Library
- Nasu, M., and Honda, N. 1968. Fuzzy events realized by finite probabilistic automata. Inf. Cont. 12, 4, 284--303.Google ScholarCross Ref
- Papoulis, A., and Pillai, S. U. 2002. Probability, Random Variables and Stochastic Processes. McGraw Hill, New York.Google Scholar
- Paxson, V. 1997. Automated packet trace analysis of TCP implementations. Computer Commun. Rev. 27, 4, 167--179. Google ScholarDigital Library
- Paz, A. 1971. Introduction to Probabilistic Automata. Academic Press, Orlando. Google ScholarDigital Library
- Perrin, D., and Pin, J.-E. 2004. Infinite Words: Automata, Semigroups, Logic and Games. Elseiver, Amesterdam, The Netherlands.Google Scholar
- Plattner, B., and Nievergelt, J. 1981. Monitoring program execution: A survey. IEEE Comput. 14, 1 (Nov.), 76--93. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Rabin, M. O. 1963. Probabilitic automata. Inf. Cont. 6, 3, 230--245.Google ScholarCross Ref
- Ranum, M. J., Landfield, K., Stolarchuk, M., Sienkiewicz, M., Lambeth, A., and Wall, E. 1997. Implementing a generalized tool for network monitoring. In Proceedings of the Systems Administration Conference. USENIX Association, 1--8. Google ScholarDigital Library
- Salomaa, A. 1973. Formal Languages. Academic Press, Orlando. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Schneider, F. B. 2000. Enforceable security policies. ACM Trans. Inf. Syst. Sec. 3, 1, 30--50. Google ScholarDigital Library
- Schroeder, B. A. 1995. Online monitoring: A tutorial. IEEE Compu., 72--78. Google ScholarDigital Library
- Sistla, A. P. 1985. On characterization of safety and liveness properties in temporal logic. In Proceedings of the ACM Symposium on Principle of Distributed Computing. ACM, New York, 39--48. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Szelepcsenyi, R. 1987. The method of forcing for nondeterministic automata. Bull. EATCS 33, 96--100.Google Scholar
- Thomas, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science. vol. B. Elsevier, Amsterdam, The Netherlands, 133--192. Google ScholarDigital Library
- Time Rover. 1997. http://www.time-rover.com.Google Scholar
- Vardi, M. 1985. Automatic verification of probabilistic concurrent systems. In Proceedings of the 26th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, 327--338. Google ScholarDigital Library
- Viswanathan, M. 2000. Foundations for the runtime analysis of software systems. Ph.D. dissertation. University of Pennsylvania. Google ScholarDigital Library
Index Terms
- On the expressiveness and complexity of randomization in finite state monitors
Recommendations
Randomization in Automata on Infinite Trees
We study finite automata running over infinite binary trees. A run of such an automaton over an input tree is a tree labeled by control states of the automaton: the labeling is built in a top-down fashion and should be consistent with the transitions of ...
Languages recognized by nondeterministic quantum finite automata
The nondeterministic quantum finite automaton (NQFA) is the only known case wherea one-way quantum finite automaton (QFA) model has been shown to be strictly superiorin terms of language recognition power to its probabilistic counterpart. We give ...
The parallel complexity of finite-state automata problems
The goal of this paper is to study the exact complexity of several important problems concerning finite-state automata and to classify the degrees of ambiguity of nondeterministic finite-state automata. Our results are as follows: (1) Minimization of ...
Comments