Synopsis
We combine first-order dynamic logic for reasoning about the possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of our dynamic logic for hybrid systems. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to nontemporal reasoning, and prove that we obtain a complete axiomatisation relative to the nontemporal base logic. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.
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
Davoren, J.M., Coulthard, V., Markey, N., Moor, T.: Non-deterministic temporal logics for general flow systems. In: Alur and Pappas [14], pp. 280–295. DOI 10.1007/b96398
Davoren, J.M., Nerode, A.: Logics for hybrid systems. IEEE 88(7), 985–1010 (2000). DOI 10.1109/5.871305
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Mitchell [210], pp. 414–425
Damm, W., Hungar, H., Olderog, E.R.: On the verification of cooperating traffic agents. In: F.S. de Boer, M.M. Bonsangue, S. Graf, W.P. de Roever (eds.) FMCO, LNCS, vol. 3188, pp. 77–110. Springer (2003). DOI 10.1007/b100112
Pratt, V.R.: Process logic. In: POPL, pp. 93–100 (1979). DOI 10.1145/567752.567761
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986). DOI 10.1145/4904.4999
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge, MA, USA (1999)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)
Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292. IEEE Computer Society, Los Alamitos (1996)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. MIT Press, Cambridge (2000)
Pnueli, A., Kesten, Y.: A deductive proof system for CTL*. In: L. Brim, P. Jancar, M. Kretínský, A. Kucera (eds.) CONCUR, LNCS, vol. 2421, pp. 24–40. Springer (2002). DOI 10.1007/3-540-45694-5_2
Reynolds, M.: An axiomatization of PCTL*. Inf. Comput. 201(1), 72–119 (2005). DOI 10.1016/j.ic.2005.03.005
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: LICS, pp. 394–406. IEEE Computer Society (1992). DOI 10.1006/inco.1994. 1045
Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982)
Mysore, V., Piazza, C., Mishra, B.: Algorithmic algebraic model checking II: Decidability of semi-algebraic model checking and its applications to systems biology. In: Peled and Tsay [226], pp. 217–233. DOI 10.1007/11562948_18
Damm, W., Hungar, H., Olderog, E.R.: Verification of cooperating traffic agents. International Journal of Control 79(5), 395–421 (2006). DOI 10.1080/00207170600587531
Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. In: Goré et al. [139], pp. 626–641. DOI 10.1007/3-540-45744-5_51
Stirling, C.: Modal and temporal logics. In: Handbook of Logic in Computer Science (vol. 2): Background: Computational Structures, pp. 477–563. Oxford University Press, Inc., New York, NY, USA (1992)
Faber, J., Meyer, R.: Model checking data-dependent real-time properties of the European Train Control System. In: FMCAD, pp. 76–77. IEEE Computer Society Press (2006). DOI 10.1109/FMCAD.2006.21
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Platzer, A. (2010). Differential Temporal Dynamic Logic dTL. In: Logical Analysis of Hybrid Systems. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14509-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-14509-4_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14508-7
Online ISBN: 978-3-642-14509-4
eBook Packages: Computer ScienceComputer Science (R0)