Skip to main content
SpringerLink
Log in
Book cover

Temporal Type Theory pp 1–15Cite as

Birkhäuser

Introduction

  • Chapter
  • First Online:

  • 920 Accesses

Part of the book series: Progress in Computer Science and Applied Logic ((PCS,volume 29))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD   59.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 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}\).

References

  1. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM (JACM) 43(1), 116–146 (1996)

    Article  MathSciNet  Google Scholar 

  2. 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)

    Google Scholar 

  3. Ashby, W.: Design for a Brain: The Origin of Adaptive Behaviour. Springer, Berlin (2013)

    MATH  Google Scholar 

  4. Åström, K.J., Wittenmark, B.: Adaptive Control. Courier Corporation, New York (2013)

    Google Scholar 

  5. Awodey, S.: Natural models of homotopy type theory. Math. Struct. Comput. Sci. 1–46 (2016). arXiv:1406.3219 [math.CT]

    Google Scholar 

  6. Bunge, M., Fiore, M.P.: Unique factorisation lifting functors and categories of linearly-controlled processes. Math. Struct. Comput. Sci. 10(2), 137–163 (2000)

    Article  MathSciNet  Google Scholar 

  7. Boileau, A., Joyal, A.: La logique des topos. J. Symb. Log. 46(1), 6–16 (1981). ISSN:0022-4812. http://dx.doi.org/10.2307/2273251

    Article  MathSciNet  Google Scholar 

  8. Coquand, T., Huet, G.: The calculus of constructions. Inform. Comput. 76(2–3), 95–120 (1988). ISSN:0890-5401. http://dx.doi.org/10.1016/0890-5401(88)90005-3

    Article  MathSciNet  Google Scholar 

  9. Fiore, M.P.: Fibred models of processes: discrete, continuous, and hybrid systems. In: IFIP TCS, vol. 1872, pp. 457–473. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Fourman, M.P.: The logic of topoi. Stud. Logic Found. Math. 90, 1053–1090 (1977)

    Article  MathSciNet  Google Scholar 

  11. Gierz, G., et al.: Continuous Lattices and Domains. Encyclopedia of Mathematics and Its Applications, vol. 93, pp. xxxvi+ 591. Cambridge University Press, Cambridge (2003). ISBN:0-521-80338-1. http://dx.doi.org/10.1017/CBO9780511542725

  12. G’alvez-Carrillo, I., Kock, J., Tonks, A.: Decomposition spaces, incidence algebras and M obius inversion I: basic theory (2015). eprint: arXiv:1512.07573

    Google Scholar 

  13. Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM (JACM) 38(4), 935–962 (1991)

    Article  MathSciNet  Google Scholar 

  14. Haghverdi, E., Tabuada, P., Pappas, G.: Bisimulation relations for dynamical and control systems. Electron. Notes Theor. Comput. Sci. 69, 120–136 (2003)

    Article  Google Scholar 

  15. Johnstone, P., Joyal, A.: Continuous categories and exponentiable toposes. J. Pure Appl. Algebra 25(3), 255–296 (1982). ISSN:0022-4049. http://dx.doi.org/10.1016/0022-4049(82)90083-4

    Article  MathSciNet  Google Scholar 

  16. Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Inform. Comput. 127(2), 164–185 (1996)

    Article  MathSciNet  Google Scholar 

  17. 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

    Google Scholar 

  18. Lawvere F.W.: State categories and response functors. Dedicated to Walter Noll. Preprint (May 1986)

    Google Scholar 

  19. 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

    Google Scholar 

  20. MacLane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, New York (1992). ISBN:0387977104

    Google Scholar 

  21. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: FORMATS/FTRTFT, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)

    Google Scholar 

  22. de Moura, L., et al.: The Lean theorem prover (system description). In: International Conference on Automated Deduction, pp. 378–388. Springer, Heidelberg (2015)

    Google Scholar 

  23. Picado, J., Pultr, A.: Frames and Locales. Frontiers in Mathematics. Topology Without Points, pp. xx+ 398. Birkhäuser/Springer Basel AG, Basel (2012). ISBN:978-3-0348-0153-9. http://dx.doi.org/10.1007/978-3-0348-0154-6

  24. Rescher, N., Urquhart, A.: Temporal Logic, vol. 3. Springer, New York (2012)

    MATH  Google Scholar 

  25. Shulman, M. Exact completions and small sheaves. Theory Appl. Categ. 27, 97–173 (2012). ISSN:1201-561X

    Google Scholar 

  26. Spivak, D.I., Vasilakopoulou, C., Schultz, P.: Dynamical Systems and Sheaves (2016). eprint: arXiv:1609.08086

    Google Scholar 

  27. Willems, J.C.: The behavioral approach to open and interconnected systems. IEEE Control Syst. 27(6), 46–99 (2007)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, MA, USA

    Patrick Schultz & David I. Spivak

Authors
  1. Patrick Schultz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David I. Spivak
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2019 The Author(s)

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Schultz, P., Spivak, D.I. (2019). Introduction. In: Temporal Type Theory. Progress in Computer Science and Applied Logic, vol 29. Birkhäuser, Cham. https://doi.org/10.1007/978-3-030-00704-1_1

Download citation

Publish with us

Policies and ethics

Search

Navigation