Abstract
Real-time systems usually encompass parts that are best described by a continuous-time model, such as physical processes under control, together with other components that are more naturally formalized by a discrete-time model, such as digital computing modules. Describing such systems in a unified framework based on metric temporal logic requires to integrate formulas which are interpreted over discrete and continuous time.
In this paper, we tackle this problem with reference to the metric temporal logic TRIO, that admits both a discrete-time and a continuous-time semantics. We identify sufficient conditions under which TRIO formulas have a consistent truth value when moving from continuous-time to discrete-time interpretations, or vice versa. These conditions basically involve the restriction to a proper subset of the TRIO language and a requirement on the finite variability over time of the basic items in the specification formulas. We demonstrate the approach with an example of specification and verification.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. JACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. In: Antsaklis [3], pp. 971–984
Antsaklis, P.J. (ed.): Special issue on hybrid systems: theory and applications. Proceedings of the IEEE 88 (2000)
Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 470–484. Springer, Heidelberg (1998)
Ciapessoni, E., Coen-Porisini, A., Crivelli, E., Mandrioli, D., Mirandola, P., Morzenti, A.: From formal models to formally-based methods: an industrial experience. ACM TOSEM 8(1), 79–113 (1999)
De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics. Formal Aspects of Computing 17(3), 319–341 (2005)
Fidge, C.J.: Modelling discrete behaviour in a continuous-time formalism. In: Proceedings of IFM 1999, pp. 170–188. Springer, Heidelberg (1999)
Furia, C.A., Rossi, M.: A compositional framework for formally verifying modular systems. ENTCS, vol. 116, pp. 185–198. Elsevier, Amsterdam (2004)
Furia, C.A., Rossi, M.: When discrete met continuous. Technical Report 2005.44, DEI, Politecnico di Milano (2005), Available from: http://www.elet.polimi.it/upload/furia/
Ghezzi, C., Mandrioli, D., Morzenti, A.: TRIO: A logic language for executable specifications of real-time systems. JSS 12(2), 107–123 (1990)
Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics: A foundation for computer science. Addison-Wesley, Reading (1994)
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Hung, D.V., Giang, P.H.: Sampling semantics of duration calculus. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 188–207. Springer, Heidelberg (1996)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)
Morzenti, A., Mandrioli, D., Ghezzi, C.: A model parametric real-time logic. ACM TOPLAS 14(4), 521–573 (1992)
Morzenti, A., Pradella, M., San Pietro, P., Spoletini, P.: Model-checking TRIO specifications in SPIN. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 542–561. Springer, Heidelberg (2003)
Ouaknine, J.: Digisation and full abstraction for dense-time model checking. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 37–51. Springer, Heidelberg (2002)
Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: Proceedings of LICS 2003, pp. 198–207. IEEE Computer Society, Los Alamitos (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Furia, C.A., Rossi, M. (2006). Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling. In: Asarin, E., Bouyer, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2006. Lecture Notes in Computer Science, vol 4202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11867340_16
Download citation
DOI: https://doi.org/10.1007/11867340_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45026-9
Online ISBN: 978-3-540-45031-3
eBook Packages: Computer ScienceComputer Science (R0)