Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Cover of the book

2019 | OriginalPaper | Chapter

1. Introduction

Authors : Patrick Schultz, David I. Spivak

Published in: Temporal Type Theory

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In this book, we provide a new mathematical formalism for proving properties about the behavior of systems. A system is a collection of interacting components, each of which may have some internal implementation that is reflected in some external behavior. This external behavior is what other neighboring systems interact with, through a shared environment. Properties of a behavior can be established over a given duration (sometimes called frame or window) of time, and we propose a mathematical language for working with these behavioral properties.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
next chapter The Interval Domain
Footnotes
1
It may be objected that these temporal logics are often Boolean whereas our topos \(\mathcal {B}\) is not; in this case, one would simply embed the statements into the Boolean subtopos \(\mathcal {B}_{\neg \neg }\subseteq \mathcal {B}\).
 
Literature
[AFH96]
[AGV71]
Artin, M., Grothendieck, A., Verdier, J.-L.: Theorie de Topos et Cohomologie Etale des Schemas I, II, III. Lecture Notes in Mathematics, vols. 269, 270, 305. Springer, Berlin (1971)
[Ash13]
Ashby, W.: Design for a Brain: The Origin of Adaptive Behaviour. Springer, Berlin (2013)MATH
[ÅW13]
Åström, K.J., Wittenmark, B.: Adaptive Control. Courier Corporation, New York (2013)
[Awo16]
Awodey, S.: Natural models of homotopy type theory. Math. Struct. Comput. Sci. 1–46 (2016). arXiv:1406.3219 [math.CT]
[BF00]
Bunge, M., Fiore, M.P.: Unique factorisation lifting functors and categories of linearly-controlled processes. Math. Struct. Comput. Sci. 10(2), 137–163 (2000)MathSciNetCrossRef
[BJ81]
[CH88]
[Fio00]
Fiore, M.P.: Fibred models of processes: discrete, continuous, and hybrid systems. In: IFIP TCS, vol. 1872, pp. 457–473. Springer, Heidelberg (2000)CrossRef
[Fou77]
[Gie+03]
[GKT15]
G’alvez-Carrillo, I., Kock, J., Tonks, A.: Decomposition spaces, incidence algebras and M obius inversion I: basic theory (2015). eprint: arXiv:1512.07573
[HS91]
[HTP03]
Haghverdi, E., Tabuada, P., Pappas, G.: Bisimulation relations for dynamical and control systems. Electron. Notes Theor. Comput. Sci. 69, 120–136 (2003)CrossRef
[JJ82]
[JNW96]
[Joh02]
Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford Logic Guides, vol. 43, pp. xxii+ 468+ 71. New York: The Clarendon Press/Oxford University Press (2002). ISBN:0-19-853425-6
[Law86]
Lawvere F.W.: State categories and response functors. Dedicated to Walter Noll. Preprint (May 1986)
[LS88]
Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol. 7, pp. x+ 293. Reprint of the 1986 original. Cambridge University Press, Cambridge (1988). ISBN:0-521-35653-9
[MM92]
MacLane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, New York (1992). ISBN:0387977104
[MN04]
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: FORMATS/FTRTFT, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)
[Mou+15]
de Moura, L., et al.: The Lean theorem prover (system description). In: International Conference on Automated Deduction, pp. 378–388. Springer, Heidelberg (2015)
[PP12]
[RU12]
Rescher, N., Urquhart, A.: Temporal Logic, vol. 3. Springer, New York (2012)MATH
[Shu12]
Shulman, M. Exact completions and small sheaves. Theory Appl. Categ. 27, 97–173 (2012). ISSN:1201-561X
[SVS16]
Spivak, D.I., Vasilakopoulou, C., Schultz, P.: Dynamical Systems and Sheaves (2016). eprint: arXiv:1609.08086
[Wil07]
Willems, J.C.: The behavioral approach to open and interconnected systems. IEEE Control Syst. 27(6), 46–99 (2007)MathSciNetCrossRef
Metadata
Title
Introduction
Authors
Patrick Schultz
David I. Spivak
Copyright Year
2019
Book
Temporal Type Theory

Print ISBN: 978-3-030-00703-4

Electronic ISBN: 978-3-030-00704-1

Copyright Year: 2019

DOI
https://doi.org/10.1007/978-3-030-00704-1_1

Premium Partner

    Image Credits