×

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.

MSC:

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

Software:

TaLiRo
PDFBibTeX XMLCite
Full Text: DOI

References:

[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, (Fifth Annual IEEE Symposium on Logic in Computer Science (1990), IEEE Computer Society Press: IEEE Computer Society Press Washington, DC) · Zbl 0791.68103
[5] Alur, R.; Torre, S. L.; Madhusudan, P., Perturbed timed automata, (Hybrid Systems: Computation and Control. Hybrid Systems: Computation and Control, LNCS, vol. 3414 (2005)) · Zbl 1078.68070
[6] Bouyer, P.; Markey, N.; Reynier, P.-A., Robust model-checking of linear-time properties in timed automata, (Correa, J. R.; Hevia, A.; Kiwi, M., Proceedings of the 7th Latin American Symposium on Theoretical Informatics (LATIN’06). Proceedings of the 7th Latin American Symposium on Theoretical Informatics (LATIN’06), of LNCS, vol. 3887 (2006), Springer: Springer Valdivia, Chile) · Zbl 1145.68464
[7] Bouyer, P.; Markey, N.; Reynier, P.-A., Robust analysis of timed automata via channel machines, (Amadio, R. M., Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures. Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures, LNCS, vol. 4962 (2008), Springer) · 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, (8th International SPIN Workshop. 8th International SPIN Workshop, LNCS, vol. 2057 (2001), Springer) · 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: MIT Press Cambridge, Massachusetts
[12] Davey, B. A.; Priestley, H. A., Introduction to Lattices and Order (2002), Cambridge University Press: 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, (Proceedings of the 31st ICALP. Proceedings of the 31st ICALP, LNCS, vol. 3142 (2004), Springer) · Zbl 1098.68092
[14] de Alfaro, L.; Manna, Z., Verification in continuous time by discrete reasoning, (Proceedings of the 4th AMAST. Proceedings of the 4th AMAST, LNCS, vol. 936 (1995), Springer) · Zbl 1496.68189
[15] Fainekos, G. E.; Girard, A.; Pappas, G. J., Temporal logic verification using simulation, (Asarin, E.; Bouyer, P., Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems. Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems, LNCS, vol. 4202 (2006), Springer) · Zbl 1141.68463
[16] Fainekos, G. E.; Girard, A.; Pappas, G. J., Hierarchical synthesis of hybrid controllers from temporal logic specifications, (Hybrid Systems: Computation and Control. Hybrid Systems: Computation and Control, LNCS, No. 4416 (2007), Springer) · Zbl 1221.93071
[17] Fainekos, G. E.; Pappas, G. J., Robustness of temporal logic specifications, (Formal Approaches to Testing and Runtime Verification. Formal Approaches to Testing and Runtime Verification, LNCS, vol. 4262 (2006), Springer) · 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); 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, (Raskin, J.-F.; Thiagarajan, P. S., Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems. Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems, LNCS, vol. 4763 (2007), Springer) · Zbl 1141.68464
[20] G.E. Fainekos, G.J. Pappas, A user guide for TaLiRo, Tech. rep., Dept. of CIS, Univ. of Pennsylvania (2008); 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, (Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic (CSL) (1999), Springer-Verlag: Springer-Verlag London, UK) · Zbl 0944.68119
[22] Furia, C. A.; Rossi, M., Integrating discrete and continuous time metric temporal logics through sampling, (Asarin, E.; Bouyer, P., Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems. Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems, LNCS, vol. 4202 (2006), Springer) · Zbl 1141.68465
[23] Furia, C. A.; Rossi, M., On the expressiveness of mtl variants over dense time, (Raskin, J.-F.; Thiagarajan, P. S., Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems. Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems, Lecture Notes in Computer Science, vol. 4763 (2007), Springer) · 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, (HART ’97: Proceedings of the International Workshop on Hybrid and Real-Time Systems (1997), Springer-Verlag: Springer-Verlag London, UK)
[26] Havelund, K.; Rosu, G., Monitoring programs using rewriting, (Proceedings of the 16th IEEE International Conference on Automated Software Engineering (2001))
[27] Henzinger, T. A., The theory of hybrid automata, (Proceedings of the 11th Annual Symposium on Logic in Computer Science (1996), IEEE Computer Society Press) · Zbl 0959.68073
[28] Henzinger, T. A.; Majumdar, R.; Prabhu, V. S., Quantifying similarities between timed systems, (FORMATS. FORMATS, LNCS, vol. 3829 (2005), Springer) · Zbl 1175.68281
[29] Henzinger, T. A.; Manna, Z.; Pnueli, A., What good are digital clocks?, (Proceedings of the 19th ICALP. Proceedings of the 19th ICALP, LNCS, vol. 623 (1992), Springer) · Zbl 1425.68255
[30] Henzinger, T. A.; Raskin, J.-F., Robust undecidability of timed and hybrid systems, (Lynch, N. A.; Krogh, B. H., Hybrid Systems: Computation and Control. Hybrid Systems: Computation and Control, LNCS, vol. 1790 (2000), Springer) · 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, (Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (2003))
[33] Julius, A. A.; Fainekos, G. E.; Anand, M.; Lee, I.; Pappas, G. J., Robust test generation and coverage for hybrid systems, (Hybrid Systems: Computation and Control. Hybrid Systems: Computation and Control, LNCS, No. 4416 (2007), Springer) · Zbl 1221.93076
[34] Kapinski, J.; Krogh, B. H.; Maler, O.; Stursberg, O., On systematic simulation of open continuous systems, (Hybrid Systems: Computation and Control. Hybrid Systems: Computation and Control, LNCS, vol. 2623 (2003), Springer) · 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, (Proceedings of the 3rd Workshop on Run-time Verification. Proceedings of the 3rd Workshop on Run-time Verification, ENTCS, vol.89 (2003))
[38] Lamine, K. B.; Kabanza, F., Reasoning about robot actions: A model checking approach, (Advances in Plan-Based Control of Robotic Agents. Advances in Plan-Based Control of Robotic Agents, LNCS, vol. 2466 (2002), Springer) · 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, (Proceedings of FORMATS-FTRTFT. Proceedings of FORMATS-FTRTFT, LNCS, vol. 3253 (2004)) · Zbl 1109.68518
[41] Markey, N.; Schnoebelen, Ph., Model checking a path (preliminary report), (Proceedings of the 14th International Conference on Concurrency Theory. Proceedings of the 14th International Conference on Concurrency Theory, LNCS, vol. 2761 (2003)) · 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, (20th IEEE Symposium on Logic in Computer Science (LICS) (2005))
[46] Pillage, L.; Rohrer, R.; Visweswariah, C., Electronic Circuit and System Simulation Methods (1995), McGraw-Hill
[47] Pnueli, A., The temporal logic of programs, (Proceedings of the 18th IEEE Symposium Foundations of Computer Science (1977)) · Zbl 0607.68022
[48] Pnueli, A., Development of hybrid systems, (Formal Techniques in Real-Time and Fault-Tolerant Systems. Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS, vol. 863 (1994), Springer) · 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, (Brinksma, E., Proceedings of the 3rd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Proceedings of the 3rd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS), LNCS, vol. 1217 (1997), Springer)
[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, (6th International Conference on Computational Methods in Systems Biology. 6th International Conference on Computational Methods in Systems Biology, LNCS, No. 5307 (2008), Springer)
[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); 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, (Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration (2004))
[54] Thati, P.; Rosu, G., Monitoring algorithms for metric temporal logic specifications, (Runtime Verification. Runtime Verification, ENTCS, vol. 113 (2005), Elsevier)
[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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.