Finite Temporal Logic Control

  • 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 treat the general problem of controlling non-deterministic finite transition systems from specifications given as LTL formulas over their sets of observations. We show that, in general, this control problem can be mapped to a Rabin game. For the particular case when the LTL formula translates to a deterministic Büchi automaton, we show that a more efficient solution to the control problem can be found via a Büchi game. Finally, for specifications given in the syntactically co-safe fragment of LTL, we show that the control problem maps to a simple reachability problem.

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