Distributed Finite-State Runtime Monitoring with Aggregated Events - Runtime Verification - page 108

References

1. Barrett, C., Stump, A., Tinelli, C.: The satisfiability modulo theories library (smt-lib) (April
2013), http://smtlib.org/
2. Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S., Stoller, S., Zadok, E., Seyster, J.: Adap-
tive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687,
pp. 168-182. Springer, Heidelberg (2013),
http://dx.doi.org/10.1007/978-3-642-35632-2_18
3. Basin, D., Klaedtke, F., Marinovic, S., Zalinescu, E.: Monitoring compliance policies over
incomplete and disagreeing logs. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687,
pp. 151-167. Springer, Heidelberg (2013),
http://dx.doi.org/10.1007/978-3-642-35632-2_17
4. Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is
ugly? In: Sokolsky, O., Ta¸ıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126-138. Springer,
Heidelberg (2007),
http://dx.doi.org/10.1007/978-3-540-77395-5_11
5. Bodden, E., Hendren, L., Lam, P., Lhotak, O., Naeem, N.A.: Collaborative runtime verifi-
cation with tracematches. In: Sokolsky, O., Ta¸ıran, S. (eds.) RV 2007. LNCS, vol. 4839,
pp. 22-37. Springer, Heidelberg (2007),
http://www.bodden.de/pubs/bhl+07collaborative.pdf
6. Bodden, E., Hendren, L., Lam, P., Lhotak, O., Naeem, N.A.: Collaborative runtime verifica-
tion with tracematches. Oxford Journal of Logics and Computation (November 2008),
http://www.bodden.de/pubs/bhl+08collaborative.pdf
7. Brzozowski, J.A.: Derivatives of regular expressions, vol. 11, pp. 481-494. ACM, New York
(1964), http://doi.acm.org/10.1145/321239.321249
8. Chen, F., Ro¸u, G.: Mop: An ecient and generic runtime verification framework. In: Pro-
ceedings of the 22nd Annual ACM SIGPLAN Conference on Object-oriented Programming
Systems and Applications, OOPSLA 2007, pp. 569-588. ACM, New York (2007),
http://doi.acm.org/10.1145/1297027.1297069
9. Miller, D., Pearson, B.: Security information and event management (SIEM) implementation.
McGraw-Hill (2011)
10. Neumann, C.: Converting deterministic finite automata to regular expressions (March 2005),
http://neumannhaus.com/christoph/papers/2005-03-16.DFA
to RegEx.pdf
11. Ste

ens, S.: P3 consulting, personal communication,
http://www.p3-consulting.de/
12. Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.:
Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS,
vol. 7186, pp. 193-207. Springer, Heidelberg (2012),
http://dx.doi.org/10.1007/978-3-642-29860-8_15

ff

A Proofs

Theorem 1 (Convergence). Given an arbitrary finite state automaton with Q states,

the transformation will always converge onto a constraint automaton whose constraint
expressions are all DCEs.
Proof. By definition, the function regex returns a regular expression of bounded size.
As Q is finite, and regex is computed pairwise for each state, the constraint automaton
will contain at most

D

2 transitions. The task is thus to show that the conversion of
regular expressions into constraints always converges onto a DCE.

| Q |