Robustness of temporal logic specifications for continuous-time signals. (English) Zbl 1186.68287

Summary: We consider the robust interpretation of Metric Temporal Logic (MTL) formulas over signals that take values in metric spaces. For such signals, which are generated by systems whose states are equipped with non-trivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. Thus, we propose multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance, \(\epsilon \), from unsatisfiability. We prove that any other signal that remains \(\epsilon \)-close to the initial one also satisfies the same MTL specification under the usual Boolean semantics. Finally, our framework is applied to the problem of testing formulas of two fragments of MTL, namely, Metric Interval Temporal Logic and closed Metric Temporal Logic, over continuous-time signals using only discrete-time analysis. The motivating idea behind our approach is that if the continuous-time signal fulfills certain conditions and the discrete-time signal robustly satisfies the temporal logic specification, then the corresponding continuous-time signal should also satisfy the same temporal logic specification.


68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic


Full Text: DOI Link


[1] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T.A.; Ho, P.-H.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theoretical computer science, 138, 1, 3-34, (1995) · Zbl 0874.68206
[2] Alur, R.; Dill, D.L., Theory of timed automata, Theoretical computer science, 126, 2, 183-235, (1994) · Zbl 0803.68071
[3] Alur, R.; Feder, T.; Henzinger, T.A., The benefits of relaxing punctuality, Journal of the ACM, 43, 116-146, (1996) · Zbl 0882.68021
[4] Alur, R.; Henzinger, T.A., Real-time logics: complexity and expressiveness, () · Zbl 0791.68103
[5] Alur, R.; Torre, S.L.; Madhusudan, P., Perturbed timed automata, () · Zbl 1078.68070
[6] Bouyer, P.; Markey, N.; Reynier, P.-A., Robust model-checking of linear-time properties in timed automata, () · Zbl 1145.68464
[7] Bouyer, P.; Markey, N.; Reynier, P.-A., Robust analysis of timed automata via channel machines, () · Zbl 1138.68431
[8] Boyd, S.; Vandenberghe, L., Convex optimization, (2004), Cambridge University Press · Zbl 1058.90049
[9] Chechik, M.; Devereux, B.; Gurfinkel, A., Model-checking infinite state-space systems with fine-grained abstractions using SPIN, () · Zbl 0985.68031
[10] Chen, C.-T., Linear system theory and design, (1998), Oxford University Press
[11] Clarke, E.M.; Grumberg, O.; Peled, D.A., Model checking, (1999), MIT Press Cambridge, Massachusetts
[12] Davey, B.A.; Priestley, H.A., Introduction to lattices and order, (2002), Cambridge University Press Cambridge, United Kingdom · Zbl 1002.06001
[13] de Alfaro, L.; Faella, M.; Stoelinga, M., Linear and branching metrics for quantitative transition systems, () · Zbl 1098.68092
[14] de Alfaro, L.; Manna, Z., Verification in continuous time by discrete reasoning, ()
[15] Fainekos, G.E.; Girard, A.; Pappas, G.J., Temporal logic verification using simulation, () · Zbl 1141.68463
[16] Fainekos, G.E.; Girard, A.; Pappas, G.J., Hierarchical synthesis of hybrid controllers from temporal logic specifications, () · Zbl 1221.93071
[17] Fainekos, G.E.; Pappas, G.J., Robustness of temporal logic specifications, () · Zbl 1186.68287
[18] G.E. Fainekos, G.J. Pappas, Robustness of temporal logic specifications for finite state sequences in metric spaces, Tech. Rep. MS-CIS-06-05, Dept. of CIS, Univ. of Pennsylvania (May 2006)
[19] Fainekos, G.E.; Pappas, G.J., Robust sampling for MITL specifications, () · Zbl 1141.68464
[20] G.E. Fainekos, G.J. Pappas, A user guide for TaLiRo, Tech. rep., Dept. of CIS, Univ. of Pennsylvania (2008)
[21] Fr√§nzle, M., Analysis of hybrid systems: an ounce of realism can save an infinity of states, () · Zbl 0944.68119
[22] Furia, C.A.; Rossi, M., Integrating discrete and continuous time metric temporal logics through sampling, () · Zbl 1141.68465
[23] Furia, C.A.; Rossi, M., On the expressiveness of mtl variants over dense time, () · Zbl 1142.68048
[24] Girard, A.; Pappas, G.J., Approximation metrics for discrete and continuous systems, IEEE transactions on automatic control, 52, 5, 782-798, (2007) · Zbl 1366.93032
[25] Gupta, V.; Henzinger, T.A.; Jagadeesan, R., Robust timed automata, ()
[26] Havelund, K.; Rosu, G., Monitoring programs using rewriting, ()
[27] Henzinger, T.A., The theory of hybrid automata, () · Zbl 0959.68073
[28] Henzinger, T.A.; Majumdar, R.; Prabhu, V.S., Quantifying similarities between timed systems, () · Zbl 1175.68281
[29] Henzinger, T.A.; Manna, Z.; Pnueli, A., What good are digital clocks?, ()
[30] Henzinger, T.A.; Raskin, J.-F., Robust undecidability of timed and hybrid systems, () · Zbl 0944.93018
[31] Hirshfeld, Y.; Rabinovich, A., Logics for real time: decidability and complexity, Fundamenta informaticae, 62, 1, 1-28, (2004) · Zbl 1127.03012
[32] Huang, J.; Voeten, J.; Geilen, M., Real-time property preservation in approximations of timed systems, ()
[33] Julius, A.A.; Fainekos, G.E.; Anand, M.; Lee, I.; Pappas, G.J., Robust test generation and coverage for hybrid systems, () · Zbl 1221.93076
[34] Kapinski, J.; Krogh, B.H.; Maler, O.; Stursberg, O., On systematic simulation of open continuous systems, () · Zbl 1032.93532
[35] Khalil, H.K., Nonlinear systems, (1996), Prentice-Hall · Zbl 0626.34052
[36] Koymans, R., Specifying real-time properties with metric temporal logic, Real-time systems, 2, 4, 255-299, (1990)
[37] Kristoffersen, K.J.; Pedersen, C.; Andersen, H.R., Runtime verification of timed LTL using disjunctive normalized equation systems, ()
[38] Lamine, K.B.; Kabanza, F., Reasoning about robot actions: A model checking approach, () · Zbl 1017.68575
[39] Luigi, I.; Johansson, K.H.; Jonsson, U.; Francesco, V., Averaging of nonsmooth systems using dither, Automatica, 42, 4, 669-676, (2006) · Zbl 1110.93044
[40] Maler, O.; Nickovic, D., Monitoring temporal properties of continuous signals, () · Zbl 1109.68518
[41] Markey, N.; Schnoebelen, Ph., Model checking a path (preliminary report), () · Zbl 1274.68197
[42] Martinon, A., Distance to the intersection of two sets, Bulletin of the Australian mathematical society, 70, 329-341, (2004) · Zbl 1072.46016
[43] Munkres, J., Topology, (1999), Prentice Hall
[44] Ogata, K., Modern control engineering, (2001), Prentice Hall
[45] Ouaknine, J.; Worrell, J., On the decidability of metric temporal logic, ()
[46] Pillage, L.; Rohrer, R.; Visweswariah, C., Electronic circuit and system simulation methods, (1995), McGraw-Hill
[47] Pnueli, A., The temporal logic of programs, () · Zbl 0607.68022
[48] Pnueli, A., Development of hybrid systems, () · Zbl 0581.68046
[49] Puri, A., Dynamical properties of timed automata, Discrete event dynamic systems, 10, 1-2, 87-113, (2000) · Zbl 0986.93042
[50] Raskin, J.-F.; Schobbens, P.-Y., Real-time logics: fictitious clock as an abstraction of dense time, ()
[51] Rizk, A.; Batt, G.; Fages, F.; Soliman, S.; Heiner, M.; Uhrmacher, A., On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology, ()
[52] B. Shults, B. Kuipers, Qualitative simulation and temporal logic: Proving properties of continuous systems, Tech. Rep. TR AI96-244, Dept. of Computer Sciences, University of Texas at Austin (January 1996) · Zbl 1017.68514
[53] Tan, L.; Kim, J.; Sokolsky, O.; Lee, I., Model-based testing and monitoring for hybrid embedded systems, ()
[54] Thati, P.; Rosu, G., Monitoring algorithms for metric temporal logic specifications, ()
[55] Wood, G.R.; Zhang, B.P., Estimation of the Lipschitz constant of a function, Journal of global optimization, 8, 1, 91-103, (1996) · Zbl 0856.90105
[56] Wulf, M.D.; Doyen, L.; Raskin, J.-F., Almost asap semantics: from timed models to timed implementations, Formal aspects of computing, 17, 3, 319-341, (2005) · Zbl 1101.68670
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.