38 H. Abbas et al.
Energy calculations.We may compute the energy consumption of an algo-
rithm that is expressed as a QRE, by viewing consumption as another quan-
tity computed by the QRE. Alternatively, we may label the transitions of the
underlying DFA by “energy terms”, and leverage analysis techniques of weighted
automata to analyze the energy consumption. Energy considerations are crucial
to implanted medical devices that must rely on a battery, and which require
surgery to replace a depleted battery.
Acknowledgments. The authors would like to thank Konstantinos Mamouras for
insightful discussions about QREs and for providing the QRE Java library we used
in this paper. This work is supported in part by AFOSR Grant FA9550-14-1-0261
and NSF Grants IIS-1447549, CNS-1446832, CNS-1446664, CNS-1445770, and CNS-
1445770, and Austrian National Research Network grants S 11405-N23 and S 11412-
N23 (RiSE/SHiNE of the FWF) and the ICT COST Action IC1402 Runtime Verifica-
tion beyond Monitoring.
References
- Alur, R., Fisman, D., Raghothaman, M.: Regular programming for quantitative
properties of data streams. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632,
pp. 15–40. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49498-1 2 - Alur, R., Freilich, A., Raghothaman, M.: Regular combinators for string trans-
formations. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL
Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth
Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS
2014, pp. 9:1–9:10. ACM, New York (2014) - Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49 (2), 172–206
(2002) - Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of
temporal logic properties. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS,
vol. 8711, pp. 23–37. Springer, Cham (2014). doi:10.1007/978-3-319-10512-3 3 - Bozzelli, L., S ́anchez, C.: Foundations of boolean stream runtime verification. In:
Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 64–79.
Springer, Cham (2014). doi:10.1007/978-3-319-11164-3 6 - Brim, L., Dluhos, P., Safr ́anek, D., Vejpustek, T.: STL-*: extending signal temporal
logic with signal-value freezing operator. Inf. Comput. 236 , 52–67 (2014) - Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.:
Temporal logic based monitoring of assisted ventilation in intensive care patients.
In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 391–403.
Springer, Heidelberg (2014). doi:10.1007/978-3-662-45231-8 30 - Chakarov, A., Sankaranarayanan, S., Fainekos, G.: Combining time and frequency
domain specifications for periodic signals. In: Khurshid, S., Sen, K. (eds.) RV
2011. LNCS, vol. 7186, pp. 294–309. Springer, Heidelberg (2012). doi:10.1007/
978-3-642-29860-8 22 - D’Angelo, B., Sankaranarayanan, S., S ́anchez, C., Robinson, W., Finkbeiner, B.,
Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous
systems. In: Proceedings of the 12th International Symposium of Temporal Rep-
resentation and Reasoning (TIME 2005), pp. 166–174. IEEE Computer Society
Press (2005)