Formal methods for discrete-time dynamical systems
Temporal logic (03B44) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to systems and control theory (93-02) Linear systems in control theory (93C05) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Discrete-time control/observation systems (93C55)
The book presents an introduction to the concept of characterizing discrete-time dynamical systems through the use of transition systems and temporal logic. This novel approach has been the cutting edge in the analysis of control systems the last decades, and this book is an excellent choice for readers being introduced to the concept. By providing the required background from the fields of dynamical systems and also formal methods, this textbook can introduce researchers from both fields to the concept of integrating formal methods and control, building up from introductory material to more advanced concepts. Thus, this work is suitable both for researchers from these fields, and also young graduates, provided they are familiar with fundamental concepts of systems theory and theoretical computer science. A strong feature of this work is its plethora of examples, which greatly help in understanding the presented theory, and also help the reader get an idea for the applications that can be considered. Part I is the introductory part of the book and presents transition systems, which are used to represent dynamical systems. Finite abstractions of systems are defined, along with simulation and bisimulation relations. Linear temporal logic and finite automata are also introduced. Part II develops model checking techniques and finite temporal logic control. Part III takes up the largest portion of the book, and is devoted to various control problems for discrete time dynamical systems, starting from the largest satisfying region and building up to advanced problems like language guided controller synthesis and optimal temporal logic control.
- scientific article; zbMATH DE number 1192216
- Formal methods for analysis of discrete systems using a specification language
- scientific article; zbMATH DE number 1273683
- Formal Verification and Synthesis for Discrete-Time Stochastic Systems
- scientific article; zbMATH DE number 1059170
- A mechanism for the formal description of dynamic systems
- scientific article; zbMATH DE number 1614646
- Formal Analysis of Discrete-Time Piecewise Affine Systems
- Formal Methods for Control of Nonlinear Systems
- A matrix-based approach to verifying stability and synthesizing optimal stabilizing controllers for finite-state automata
- Optimal multirate sampling in symbolic models for incrementally stable switched systems
- Synthesis of minimally restrictive optimal stability-enforcing supervisors for nondeterministic discrete event systems
- A survey of challenges for runtime verification from advanced application domains (beyond software)
- On distributed symbolic control of interconnected systems under persistency specifications
- Quadratic maximization of reachable values of affine systems with diagonalizable matrix
- Lazy controller synthesis for monotone transition systems and directed safety specifications
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Robustly complete finite-state abstractions for verification of stochastic systems
- Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
- Compositional construction of abstractions for infinite networks of discrete-time switched systems
- Decentralized route-planning for multi-vehicle teams to satisfy a subclass of linear temporal logic specifications
- Abstraction-based synthesis for stochastic systems with omega-regular objectives
- Similarity quantification for linear stochastic systems: a coupling compensator approach
- Linear temporal logic for hybrid dynamical systems: characterizations and sufficient conditions
- Compositional construction of infinite abstractions for networks of stochastic control systems
- Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions
- Computation of the maximal invariant set of discrete-time linear systems subject to a class of non-convex constraints
- Least-violating symbolic controller synthesis for safety, reachability and attractivity specifications
- Symbolic control design of incrementally stable nonlinear systems with dynamic regular language specifications
- Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications
- Formal controller synthesis from specifications given by discrete-time hybrid automata
- Abstraction-based control synthesis using partial information
- Temporal logic guided safe model-based reinforcement learning: a hybrid systems approach
- Linear temporal logic satisfaction in adversarial environments using secure control barrier certificates
- scientific article; zbMATH DE number 1059170 (Why is no real title available?)
- Digital bifurcation analysis of Internet congestion control protocols
- Formal Methods for Control of Nonlinear Systems
- Safe learning-based model predictive control using the compatible models approach
- Adaptive strategies for rLTL games
- Robust stutter bisimulation for abstraction and controller synthesis with disturbance
- Formal methods to comply with rules of the road in autonomous driving: state of the art and grand challenges
- Switching controller synthesis for delay hybrid systems under perturbations
- Model-based reinforcement learning for approximate optimal control with temporal logic specifications
- Distributionally Robust Strategy Synthesis for Switched Stochastic Systems
- SySCoRe: Synthesis via Stochastic Coupling Relations
- Dynamic event-triggered prescribed performance control for nonlinear systems with signal temporal logic
- A direct symbolic algorithm for solving stochastic Rabin games
- Synthesizing permissive winning strategy templates for parity games
- Data-driven verification and synthesis of stochastic systems via barrier certificates
- Time minimization and online synchronization for multi-agent systems under collaborative temporal logic tasks
- Formal controller synthesis for Markov jump linear systems with uncertain dynamics
- Data-driven abstraction-based control synthesis
- A mobile robot controller using reinforcement learning under scLTL specifications with uncertainties
- Multiple tasks control of nonlinear systems under signal temporal logic and its application to mobile robots
- Decentralized control of finite state systems: a game theoretic approach
- Symbolic control: unveiling free robustness margins
- A leader-follower communication protocol for motion planning in partially known environments under temporal logic specifications
- SySCcoRe 2.0: toolset for formal control synthesis of continuous-state stochastic systems and temporal logic specifications
- Solving odd-fair parity games
- Context-triggered games for reactive synthesis over stochastic systems via control barrier certificates
- CTL model checking of MDPs over distribution spaces: algorithms and sampling-based computations
- Memoryless concretization relation
- Contract-based distributed logical controller synthesis
- Quadratic maximization of reachable values of stable discrete-time affine systems
- Extensions of \(\mathcal{KL}\) and Lyapunov functions for discrete-time dynamical system peak analysis
- On robust supervisory control of metric discrete event systems for scLTL specifications
- Kernel-based learning of safety barriers
- Contract-based multi-agent logical controller synthesis under uncertainty
- Network assurance via hybrid systems modelling and set invariance
- Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability
This page was built for publication: Formal methods for discrete-time dynamical systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2012356)
