Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
In general, the control function \(\varOmega \) is a partial function, i.e. not every finite sequence of states is mapped to an input.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Belta, C., Yordanov, B., Aydin Gol, E. (2017). Finite Temporal Logic Control. In: Formal Methods for Discrete-Time Dynamical Systems. Studies in Systems, Decision and Control, vol 89. Springer, Cham. https://doi.org/10.1007/978-3-319-50763-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-50763-7_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-50762-0
Online ISBN: 978-3-319-50763-7
eBook Packages: EngineeringEngineering (R0)