Abstract
We survey some of the problems associated with checking whether a given behavior (a sequence, a Boolean signal or a continuous signal) satisfies a property specified in an appropriate temporal logic and describe two such monitoring algorithms for the real-time logic MITL.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abarbanel, Y., et al.: FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 538–542. Springer, Heidelberg (2000)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The Benefits of Relaxing Punctuality. Journal of the ACM 43, 116–146 (1996)
Alur, R., Henzinger, T.A.: Logics and Models of Real-Time: A Survey. In: Huizing, C., et al. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)
Asarin, E.: Challenges in Timed Languages. Bulletin of EATCS 83 (2004)
Asarin, E., Caspi, P., Maler, O.: Timed Regular Expressions. The Journal of the ACM 49, 172–206 (2002)
Beer, I., et al.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, Springer, Heidelberg (2001)
Bensalem, S., et al.: Testing Conformance of Real-time Applications with Automatic Generation of Observers. In: RV 2004 (2004)
Donzé, A.: Etude d’un Modèle de Contrôleur Hybride. Master’s thesis, INPG (2003)
Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)
Eisner, C., et al.: Reasoning with Temporal Logic on Truncated Paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)
Geilen, M.C.W., Dams, D.R.: An On-the-fly Tableau Construction for a Real-time Temporal Logic. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 276–290. Springer, Heidelberg (2000)
Geilen, M.C.W.: Formal Techniques for Verification of Complex Real-time Systems, PhD thesis, Eindhoven University of Technology (2002)
Geilen, M.C.W.: An Improved On-the-fly Tableau Construction for a Real-time Temporal Logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 394–406. Springer, Heidelberg (2003)
Havelund, K., Rosu, G. (eds.): Runtime Verification RV 2002. ENTCS 70(4) (2002)
Havelund, K., Rosu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)
Henzinger, T.A.: It’s about Time: Real-time Logics Reviewed. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 439–454. Springer, Heidelberg (1998)
Hirshfeld, Y., Rabinovich, A.: Logics for Real Time: Decidability and Complexity. Fundamenta Informaticae 62, 1–28 (2004)
Kesten, Y., Pnueli, A.: A Compositional Approach to CTL* Verification. Theoretical Computer Science 331, 397–428 (2005)
Kossentini C., Caspi, P.: Approximation, Sampling and Voting in Hybrid Computing Systems, HSCC (to appear, 2006)
Koymans, R.: Specifying Real-time Properties with with Metric Temporal Logic. Real-time Systems, 255–299 (1990)
Kim, M., et al.: Monitoring, Checking, and Steering of Real-time Systems. RV 2002, ENTCS 70(4) (2002)
Kristoffersen, K.J., Pedersen, C., Andersen, H.R.: Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems. RV 2003 ENTCS 89(2) (2003)
Krichen, M., Tripakis, S.: Black-box Conformance Testing for Real-time Systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 109–126. Springer, Heidelberg (2004)
Kupferman, O., Vardi, M.Y.: On Bounded Specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 24–38. Springer, Heidelberg (2001)
Mosterman, P.J.: An Overview of Hybrid Simulation Phenomena and their Support by Simulation Packages. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 165–177. Springer, Heidelberg (1999)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The Glory of the Past. In: LCTES 2000. LNCS, pp. 196–218 (1985)
Maler, O.: A Unified Approach for Studying Discrete and Continuous Dynamical Systems. In: CDC, pp. 2083–2088. IEEE, Los Alamitos (1998)
Maler, O.: Control from Computer Science. Annual Reviews in Control 26, 175–187 (2002)
Maler, O.: Analog Circuit Verification: a State of an Art. ENTCS 153, 3–7 (2006)
Maler, O., Nickovic, D.: Monitoring Temporal Properties of Continuous Signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)
Maler, O., Nickovic, D., Pnueli, A.: Real Time Temporal Logic: Past, Present, Future. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 2–16. Springer, Heidelberg (2005)
Maler, O., Nickovic, D., Pnueli, A.: From MITL to Timed Automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006)
Maler, O., Nickovic, D., Pnueli, A.: On Synthesizing Controllers from Bounded-Response Properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 95–107. Springer, Heidelberg (2007)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, Heidelberg (1992)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)
Nickovic, D., Maler, O.: AMT: A Property-Based Monitoring Tool for Analog Systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304–319. Springer, Heidelberg (2007)
Safra, S.: On the Complexity of ω-Automata. In: FOCS 1988, pp. 319–327 (1988)
Sokolsky, O., Viswanathan, M.(eds.): Runtime Verification RV 2003. ENTCS 89(2) (2003)
Trakhtenbrot, B.A.: Finite Automata and the Logic of One-place Predicates. DAN SSSR 140 (1961)
Thati, P., Rosu, G.: Monitoring Algorithms for Metric Temporal Logic Specifications. RV (2004)
Tripakis, S.: Fault Diagnosis for Timed Automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 205–224. Springer, Heidelberg (2002)
Vardi, M.Y., Wolper, P.: An Automata-theoretic Approach to Automatic Program Verification. In: LICS 1986, pp. 322–331. IEEE, Los Alamitos (1986)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Maler, O., Nickovic, D., Pnueli, A. (2008). Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds) Pillars of Computer Science. Lecture Notes in Computer Science, vol 4800. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78127-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-78127-1_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78126-4
Online ISBN: 978-3-540-78127-1
eBook Packages: Computer ScienceComputer Science (R0)