Information Technology Reference
In-Depth Information
5Conluon
In this paper, we investigated the problem of monitoring visibly context-free
properties. In particular we proposed a four-valued semantics for the future
fragment of the temporal logic CaRet on finite words, together with a mon-
itor synthesis algorithm yielding deterministic push-down Mealy machines for
properties with calls and returns.
For the full CaRet logic, or more generally, for any visibly context-free lan-
guage, we provided a three-valued monitoring approach adhering both, to the
maxims of impartiality and anticipation. It comprises a three-valued anticipatory
semantics as well as corresponding synthesis algorithm yielding deterministic
push-down Moore machine.
Together with [17] this gives a complete picture of two-valued, impartial and
anticipatory semantics for runtime monitoring.
References
1. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr.
Program. 78(5), 293-303 (2009)
2. Chen, F., Rosu, G.: Mop: an e
cient and generic runtime verification framework. In:
Gabriel, R.P., Bacon, D.F., Lopes, C.V., G.L.S. Jr. (eds.) OOPSLA, pp. 569-588.
ACM (2007)
3. Bauer, A., Leucker, M., Schallhart, C.: Comparing ltl semantics for runtime veri-
fication. J. Log. Comput. 20(3), 651-674 (2010)
4. Leucker, M.: Teaching runtime verification. In: Khurshid, S., Sen, K. (eds.) RV 2011.
LNCS, vol. 7186, pp. 34-48. Springer, Heidelberg (2012)
5. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46-57. IEEE Computer
Society (1977)
6. Geilen, M.: On the construction of monitors for temporal logic properties. Electr.
Notes Theor. Comput. Sci. 55(2), 181-199 (2001)
7. Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: ASE, pp. 135-143.
IEEE Computer Society (2001)
8. Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Katoen,
J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342-356. Springer,
Heidelberg (2002)
9. D'Amorim, M., Rosu, G.: Ecient monitoring of
ω
languages. In: Etessami, K.,
Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364-378. Springer,
Heidelberg (2005)
10. Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-
Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260-272. Springer,
Heidelberg (2006)
11. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for ltl and tltl. ACM
Trans. Softw. Eng. Methodol. 20(4), 14 (2011)
12. Dong, W., Leucker, M., Schallhart, C.: Impartial anticipation in runtime-
verification. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.)
ATVA 2008. LNCS, vol. 5311, pp. 386-396. Springer, Heidelberg (2008)
13. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC,
pp. 202-211. ACM (2004)
