Temporal Logics and Automata

  • Calin BeltaEmail author
  • Boyan Yordanov
  • Ebru Aydin Gol
Part of the Studies in Systems, Decision and Control book series (SSDC, volume 89)


In this chapter, we introduce the syntax and semantics of Linear Temporal Logic (LTL) and of one of its fragments, called syntactically co-safe LTL (scLTL), and we illustrate them through several examples.We also define the automata that will be later used for system analysis and control from such specifications.


Model Check Linear Temporal Logic Finite State Automaton Computation Tree Logic Input Alphabet 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Mechanical Engineering, Electrical and Computer Engineering, and Systems EngineeringBoston UniversityBostonUSA
  2. 2.Biological Computation GroupMicrosoft Research LtdCambridgeUK
  3. 3.Department of Computer EngineeringMiddle East Technical UniversityCankayaTurkey

Personalised recommendations