Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2017 | Buch

Transition Systems Kapitel lesen Erstes Kapitel lesen

Formal Methods for Discrete-Time Dynamical Systems

verfasst von: Calin Belta, Boyan Yordanov, Ebru Aydin Gol

Verlag: Springer International Publishing

Buchreihe : Studies in Systems, Decision and Control

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book bridges fundamental gaps between control theory and formal methods. Although it focuses on discrete-time linear and piecewise affine systems, it also provides general frameworks for abstraction, analysis, and control of more general models.
The book is self-contained, and while some mathematical knowledge is necessary, readers are not expected to have a background in formal methods or control theory. It rigorously defines concepts from formal methods, such as transition systems, temporal logics, model checking and synthesis. It then links these to the infinite state dynamical systems through abstractions that are intuitive and only require basic convex-analysis and control-theory terminology, which is provided in the appendix. Several examples and illustrations help readers understand and visualize the concepts introduced throughout the book.

Inhaltsverzeichnis

Frontmatter

Transition Systems, Automata, and Temporal Logics

Frontmatter
Chapter 1. Transition Systems
Abstract
In this chapter, we define the syntax and semantics of transition systems, and provide several illustrative examples. In particular, we present different (deterministic, nondeterministic, finite, and infinite) transition system representations for discrete-time dynamical systems. We also introduce simulation and bisimulation relations, which are central for the construction of finite abstractions throughout the book.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 2. Temporal Logics and Automata
Abstract
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.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol

Analysis and Control of Finite Transition Systems

Frontmatter
Chapter 3. Model Checking
Abstract
In this chapter, we introduce model checking, which is the most basic analysis problem in formal verification. As the focus of the book is on LTL, we restrict our attention to LTL specifications. Since we focus on analysis, we consider transition systems with no inputs. Informally, the LTL model checking problem consists of determining whether the language originating at a state of a finite transition system satisfies an LTL formula over its set of observations. The algorithms presented in this chapter will be extended in subsequent chapters to solve more difficult problems, such as finding the largest satisfying region for finite transition systems and infinite transition systems embedding discrete-time dynamical systems.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 4. Largest Finite Satisfying Region
Abstract
In this chapter, we focus on the problem of analyzing a finite transition system with the goal of partitioning its state space into satisfying and non-satisfying subsets of states. Since the focus is on analysis, we consider transition systems with no inputs.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 5. Finite Temporal Logic Control
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.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol

Analysis and Control of Discrete-Time Dynamical Systems

Frontmatter
Chapter 6. Discrete-Time Dynamical Systems
Abstract
In this chapter, we introduce the two classes of discrete-time dynamical systems that we will focus on in the rest of the book: piecewise affine control systems with polytopic parameter uncertainties and switched linear systems. As particular instantiations of the first class, we define autonomous systems, fixed parameter systems, and combinations of the above. We define embeddings of such systems into (infinite) transition systems. This enables formal definitions for their semantics and the use of abstractions to map analysis and control problems for such systems to verification and synthesis problems for finite transition systems.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 7. Largest Satisfying Region
Abstract
In this chapter, we develop a procedure that attempts to find the largest set of initial states from which an autonomous PWA system satisfies an LTL formula over the set labeling the polytopes in its definition. We formulate the problem for the general case of autonomous PWA systems with uncertain parameters, and we show that more efficient solutions can be found for the particular cases of autonomous PWA systems with fixed parameters and additive uncertainties.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 8. Parameter Synthesis
Abstract
In this chapter, we we study autonomous PWA systems with uncertain parameters. The parameters of the system are allowed to vary in predefined polytopic ranges. In this chapter we assume that those ranges can be restricted further. In other words, we treat the parameter ranges not as an uncertainty inherent in the system, but rather as allowed ranges in which the system parameters must be tuned. Our goal is to find subsets of the allowed parameters for each region, such that the satisfaction of a specification can be guaranteed.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 9. Temporal Logic Control
Abstract
Unlike the systems we discussed in previous chapters, which evolved autonomously, in this chapter we consider PWA control systems, which can be affected externally by applying a control signal. Then, it is possible to guarantee the satisfaction of a specification by trajectories of a PWA control system if an appropriate control signal is applied. We focus on fixed-parameter, PWA control systems. In Chap. 5 we discussed the problem of controlling a finite, possibly nondeterministic transition system from LTL specifications. To apply the methods presented there, in this chapter we develop an approach based on the construction of a finite abstraction for the infinite embedding of the PWA system, followed by the generation of a control strategy for the abstraction.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 10. Finite Bisimulations
Abstract
In this chapter, we focus on verification and control of switched linear systems. We show that a finite bisimulation quotient of a stable switched linear system exists and can be constructed by performing a finite number of basic polyhedral operations. To construct the quotient system, we use a polyhedral Lyapunov function. The existence of such a function is a necessary condition for the stability of a switched linear system. Once a bisimulation quotient is constructed, the verification and synthesis problems can be solved by using techniques presented in Chaps. 4 and 5.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 11. Language Guided Controller Synthesis
Abstract
In Chap. 9, we treated the temporal logic control problem for a PWA system.While being able to accommodate full LTL specifications, the method from Chap. 9 was conservative, mainly because the original (rough) partition of the state space was not refined if a control strategy was not found. In this chapter, we address this limitation. We restrict our attention to specifications given in the co-safe fragment of LTL (scLTL) and present a language-guided synthesis method. Central to our approach is the construction and refinement of an automaton that restricts the search for initial states and control strategies in such a way that the satisfaction of the specification is guaranteed at all times. We focus on fixed-parameter control PWA systems.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Chapter 12. Optimal Temporal Logic Control
Abstract
In this chapter, we focus on synthesis of an optimal control strategy for a PWA system constrained to satisfy a temporal logic specification. The specification is a formula of syntactically co-safe Linear Temporal Logic (scLTL). The cost is a quadratic function that penalizes the distance from desired state and control trajectories, which are called reference trajectories. To incorporate dynamic environments, we assume that the reference trajectories are only available over a finite horizon. The goal is to find a control strategy such that the trajectory of the closed-loop system originating from a given initial state satisfies the formula and minimizes the cost. We treat the temporal logic specifications as constraints in an optimal control problem and propose a model predictive control (MPC) solution, as the natural approach for such constrained problems.
Calin Belta, Boyan Yordanov, Ebru Aydin Gol
Backmatter
Metadaten
Titel
Formal Methods for Discrete-Time Dynamical Systems
verfasst von
Calin Belta
Boyan Yordanov
Ebru Aydin Gol
Copyright-Jahr
2017
Electronic ISBN
978-3-319-50763-7
Print ISBN
978-3-319-50762-0
DOI
https://doi.org/10.1007/978-3-319-50763-7

Neuer Inhalt

    Bildnachweise