Zusammenfassung
Die TL ist unentbehrlich für die formale Verifikation von Realzeitsystemen. Der modale Begriff der Notwendigkeit kann temporal als „immer“ interpretiert werden. Es geht dabei um logische Bezüge zwischen Aktionen, die zumeist auf eine spezielle Form der temporalen Quantifizierung hinauslaufen. Die TL ist dabei flexibler als eine reine Darstellung von Tatsachen durch die PL.
In diesem Kapitel werden mehrere Kalküle vorgestellt, von der klassischen einfachen Minimal Tense Logic bis hin zum modernen, sehr eleganten und aussagekräftigen Duration Calculus.
Auf der Ebene der Kripke-Semantiken für eine modale temporale Logik lassen sich die Zeitdomänen sehr gut an die praktischen Bedürfnisse anpassen:
-
als Äquivalenzrelation oder mit schwächeren relationalen Eigenschaften,
-
als totale Ordnung oder als verzweigende Zeit, wie in parallelen Systemen angemessen,
-
mit diskreter oder kontinuierlicher Zeit,
-
mit metrisierbarer Zeit, also mit genau messbaren Zeitangaben.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Et sic quidquid semper est, non contingenter semper est, sed ex necessitate. (I de Caelo, lect.26, n.258.)
- 2.
De Potentia Dei, O.3, Art.1, Obj.17 (zitiert nach Kripke 1971)
Literatur
Hansen, M.R., Zhou, C.: Lecture notes on logical foundations of duration calculus. Formal Aspects of Computing (1996)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time. Syst. 2(4):255–299 (1990)
Kripke, S.A.: Naming and necessity. In: Davidson, D., Harman, G. (Hrsg) (1972) Semantics of Natural Language. D. Reidel, Dordrecht, S 253–355. Übers. v. Wolf U (1981) Name und Notwendigkeit. Frankfurt am Main (1971)
Lyons, J.: Semantics, Vol. 2. Cambridge University Press, Cambridge (1977)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)
Moszkowski, B.: Executing temporal logic programs. Cambridge University Press, Cambridge (1986)
Prior, A.N.: Past, present and future. Clarendon Press, Oxford (1967)
Zhou, C., Hansen, M.R.: Duration calculus: A formal approach to real-time systems. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2003)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2013 Springer Fachmedien Wiesbaden
About this chapter
Cite this chapter
Schenke, M. (2013). Temporale Logik. In: Logikkalküle in der Informatik. Studienbücher Informatik. Springer Vieweg, Wiesbaden. https://doi.org/10.1007/978-3-8348-2295-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-8348-2295-6_7
Published:
Publisher Name: Springer Vieweg, Wiesbaden
Print ISBN: 978-3-8348-1887-4
Online ISBN: 978-3-8348-2295-6
eBook Packages: Computer Science and Engineering (German Language)