Abstract
We present a technique for generating efficient monitors for ω-regular-languages. We show how Büchi automata can be reduced in size and transformed into special, statistically optimal nondeterministic finite state machines, called binary transition tree finite state machines (BTT-FSMs), which recognize precisely the minimal bad prefixes of the original ω-regular-language. The presented technique is implemented as part of a larger monitoring framework and is available for download.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
MOP website, LTL plugin, http://fsl.cs.uiuc.edu/mop/repository.jsp?ltype=LTL
Artho, C., Drusinsky, D., Goldberg, A., Havelund, K., Lowry, M., Păsăreanu, C., Roşu, G., Visser, W., Washington, R.: Automated Testing using Symbolic Execution and Temporal Monitoring. Theoretical Computer Sci. (2005) (to appear)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)
Beer, I., Ben-David, S., Landver, A.: On-the-Fly Model Checking of RCTL Formulas. In: CAV 1998, pp. 184–194. Springer, Heidelberg (1998)
Büchi, J.R.: On a Decision Method in Restricted Second Order Arithmetic. In: Logic, Methodology and Philosophy of Sciences. Stanford University Press, Stanford (1962)
Chen, F., d’Amorim, M., Roşu, G.: A Formal Monitoring-Based Framework for Software Development and Analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 357–372. Springer, Heidelberg (2004)
Chen, F., Roşu, G.: Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. In: Proceedings of RV 2003. ENTCS, vol. 89, pp. 106–125 (2003)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
d’Amorim, M., Roşu, G.: Efficient monitoring of ω-languages. Technical Report UIUCDCS-R-2005-2530, University of Illinois Urbana-Champaign (March 2005)
Dudani, S., Geada, J., Jakacki, G., Vainer, D.: Dynamic Assertions Using TXP. ENTCS, vol. 55(2) (2001)
Etessami, K., Holzmann, G.: Optimizing Büchi Automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)
Ezick, J.: An Optimizing Compiler for Batches of Temporal Logic Formulas. In: Proceedings of ISSTA 2004, pp. 183–194. ACM Press, New York (2004)
Gastin, P., Oddoux, D.: LTL with Past and Two-Way Very-Weak Alternating Automata. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 439–448. Springer, Heidelberg (2003)
Geilen, M.: On the Construction of Monitors for Temporal Logic Properties. In: Proceedings of RV 2001. ENTCS, vol. 55. Elsevier Science, Amsterdam (2001)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly Automatic Verification of Linear Temporal Logic. In: Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, pp. 3–18. Chapman & Hall, Ltd., Boca Raton (1996)
Havelund, K., Roşu, G.: Monitoring Java Programs with Java PathExplorer. In: Proceedings of RV 2001. ENTCS, vol. 55. Elsevier Science, Amsterdam (2001)
Havelund, K., Roşu, G.: Workshops on Runtime Verification (RV 2001, RV 2002, RV 2004). ENTCS, vol. 55, 70(4). Elsevier, Amsterdam (2001, 2002, 2004) (to appear)
Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)
Holzmann, G.: The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A Decision Algorithm for Full Propositional Temporal Logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 97–109. Springer, Heidelberg (1993)
Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a Run-time Assurance Tool for Java. In: Proceedings of RV 2001. ENTCS, vol. 55. Elsevier Sci., Amsterdam (2001)
Kupferman, O., Vardi, M.Y.: Model Checking of Safety Properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172–183. Springer, Heidelberg (1999)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Markey, N.: Temporal Logic with Past is Exponentially more Succinct. EATCS Bulletin 79, 122–128 (2003)
Moret, B.: Decision Trees and Diagrams. ACM Comp. Surv. 14(4), 593–623 (1982)
Oddoux, D., Gastin, P.: LTL2BA, http://www.liafa.jussieu.fr/~oddoux/ltl2ba/
Roşu, G., Havelund, K.: Rewriting-Based Techniques for Runtime Verification. Journal of Automated Software Engineering 12(2), 151–197 (2005)
Ruf, J., Hoffmann, D., Kropf, T., Rosenstiel, W.: Simulation-Guided Property Checking Based on Multi-Valued AR-Automata. In: Proceedings of DATE 2001, London, UK, pp. 742–749. IEEE Computer Society Press, Los Alamitos (2001)
Sen, K., Roşu, G., Agha, G.: Online Efficient Predictive Safety Analysis of Multithreaded Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 123–138. Springer, Heidelberg (2004)
Sistla, A.P., Clarke, E.M.: The Complexity of Propositional Linear Temporal Logics. Journal of the ACM 32(3), 733–749 (1985)
Sokolsky, O., Viswanathan, M.: Workshop on Runtime Verification (RV 2003). ENTCS, vol. 89. Elsevier, Amsterdam (2003)
Thati, P., Roşu, G.: Monitoring Algorithms for Metric Temporal Logic. In: Proceedings of RV 2004. ENTCS, Elsevier Science, Amsterdam (2004) (to appear)
Wolper, P.: Constructing Automata from Temporal Logic Formulas: a Tutorial. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 261–277. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
d’Amorim, M., Roşu, G. (2005). Efficient Monitoring of ω-Languages. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_36
Download citation
DOI: https://doi.org/10.1007/11513988_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)