Abstract
Runtime verification techniques allow us to monitor an execution and check whether it satisfies some given property. Efficiency in runtime verification is of critical importance, because the evaluation is performed while new events are monitored. We apply runtime verification to obtain quantitative information about the execution, based on linear-time temporal properties: the temporal specification is extended to include parameters that are instantiated according to a measure obtained at runtime. The measure is updated in order to maintain the best values of parameters, according to their either maximizing or minimizing behavior, and priority. We provide measuring algorithms for linear-time temporal logic with parameters (PLTL). Our key result is that achieving efficient runtime verification is dependent on the determinization of the measuring semantics of PLTL. For deterministic PLTL, where all disjunctions are guarded by atomic propositions, online measuring requires only linear space in the size of the specification and logarithmic space in the length of the trace. For unambiguous PLTL, where general disjunctions are allowed, but the measuring is deterministic in the truth values of the non-parametric subformulas, the required space is exponential in the size of the specification, but still logarithmic in the length of the trace. For full PLTL, we show that online measuring is inherently hard and instead provide an efficient offline algorithm.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime Monitoring of Synchronous Systems. In: TIME 2005, pp. 166–174 (2005)
Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for “model measuring”. ACM Trans. Comput. Log. 2(3), 388–407 (2001)
Bauer, A., Leucker, M., Schallhart, C.: Runtime Verification for LTL and TLTL. ACM Trans. Software Engineering Methodologies 20(4), 14 (2011)
Etessami, K.: A note on a question of Peled and Wilke regarding stutter-invariant LTL. Information Processing Letters 75, 261–263 (2000)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995, pp. 3–18 (1995)
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)
Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting statistics over runtime executions. Proceedings of Runtime Verification (RV 2002), Electronic Notes in Theoretical Computer Science 70(4), 36–54 (2002)
Finkbeiner, B., Sipma, H.: Checking Finite Traces Using Alternating Automata. Formal Methods in System Design 24(2), 101–127 (2004)
Kupferman, O., Piterman, N., Vardi, M.Y.: From Liveness to Promptness. Formal Methods in System Design 34(2), 83–103 (2009)
Kupferman, O., Vardi, M.Y.: Model Checking of Safety Properties. Formal Methods in System Design 19(3), 291–314 (2001)
Maidl, M.: The Common Fragment of CTL and LTL. In: FOCS 2000, Rodendo Beach, CA, USA, pp. 643–652 (2000)
Manna, Z., Pnueli, A.: Completing the Temporal Picture. Theoretical Computer Science 83, 91–130 (1991)
Pnueli, A., Zaks, A.: PSL Model Checking and Run-Time Verification Via Testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)
Rosu, G., Chen, F.: Semantics and Algorithms for Parametric Monitoring. Logical Methods in Computer Science 8, 1 (2012)
Vardi, M., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: LICS 1986, Cambridge, MA, pp. 332–344 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Faymonville, P., Finkbeiner, B., Peled, D. (2014). Monitoring Parametric Temporal Logic. In: McMillan, K.L., Rival, X. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2014. Lecture Notes in Computer Science, vol 8318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54013-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-54013-4_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54012-7
Online ISBN: 978-3-642-54013-4
eBook Packages: Computer ScienceComputer Science (R0)