A5091718585- Formal Methods in Verification
- Petri Nets in System Modeling
- Advanced Control Systems Optimization
- Software Reliability and Analysis Research
- Fault Detection and Control Systems
- Gene Regulatory Network Analysis
- Simulation Techniques and Applications
- Reinforcement Learning in Robotics
- Embedded Systems Design Techniques
- Bayesian Modeling and Causal Inference
- Model-Driven Software Engineering Techniques
- Adversarial Robustness in Machine Learning
- Machine Learning and Algorithms
- Safety Systems Engineering in Autonomy
- Smart Grid Energy Management
- Real-Time Systems Scheduling
- Stability and Control of Uncertain Systems
- Software Testing and Debugging Techniques
- Model Reduction and Neural Networks
- Risk and Safety Analysis
- Control Systems and Identification
- Probabilistic and Robust Engineering Design
- Building Energy and Comfort Optimization
- Advanced Software Engineering Methodologies
- Logic, Reasoning, and Knowledge
University of Oxford
2015-2024
Peking University
2024
Science Oxford
2015-2023
The Alan Turing Institute
2023
Turing Institute
2023
British Library
2023
Sepuluh Nopember Institute of Technology
2017-2020
Delft University of Technology
2009-2015
Eindhoven University of Technology
2015
Max Planck Institute for Software Systems
2015
Symbolic approaches for control design construct finite-state abstract models that are related to the original systems, then use techniques from synthesis compute controllers satisfying specifications given in a temporal logic, and finally translate synthesized schemes back as systems. Such have been successfully developed implemented of over non-probabilistic In this paper, we extend technique probabilistic systems modelled by controlled stochastic differential equations. We show every...
This work is concerned with the generation of finite abstractions general state-space processes to be employed in formal verification probabilistic properties by means automatic techniques such as model checkers. The employs an abstraction procedure based on partitioning state-space, which generates a Markov chain approximation original process. A novel adaptive and sequential gridding algorithm presented expected conform underlying dynamics thus mitigate curse dimensionality unavoidably...
We present a model-free reinforcement learning algorithm to synthesize control policies that maximize the probability of satisfying high-level objectives given as Linear Temporal Logic (LTL) formulas. Uncertainty is considered in workspace properties, structure workspace, and agent actions, giving rise Probabilistically-Labeled Markov Decision Process (PL-MDP) with unknown graph stochastic behaviour, which even more general than fully MDP. first translate LTL specification into Limit...
This paper discusses a two-step procedure, based on the use of formal abstractions, to generate finite-space stochastic dynamical model as an aggregation continuous temperature dynamics homogeneous population thermostatically controlled loads (TCLs). The TCL is described by difference equation and status (ON, OFF) deterministic switching mechanism. procedure deemed be formal, it allows quantification error introduced abstraction. As such, builds improves known, earlier approximation...
We propose an automatic and formally sound method for synthesising Lyapunov functions the asymptotic stability of autonomous non-linear systems. Traditional methods are either analytical require manual effort or numerical but lack formal soundness. Symbolic computational functions, which in between, give guarantees typically semi-automatic because they rely on user to provide appropriate function templates. a that finds fully automatically$-$using machine learning$-$while also providing...
<para xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"> In this paper, we derive some important properties for the finite-horizon and infinite-horizon value functions associated with discrete-time switched LQR (DSLQR) problem. It is proved that any function of DSLQR problem pointwise minimum a finite number quadratic can be obtained recursively using so-called <emphasis emphasistype="italic">switched Riccati mapping</emphasis>. also shown under mild...
This paper studies the quadratic regulation problem for discrete-time switched linear systems (DSLQR problem) on an infinite time horizon. A general relaxation framework is developed to simplify computation of value iterations. Based this framework, efficient algorithm solve infinite-horizon DSLQR with guaranteed closed-loop stability and suboptimal performance. Due these guarantees, proposed can be used as a controller synthesis tool systems.
Residential thermostatically controlled loads (TCLs) have potential for participation in electricity markets. This is because we can control a large group of these to achieve aggregate system behavior such as providing frequency reserves while ensuring the actions are non-disruptive end users. A main challenge controlling aggregations TCLs developing dynamical models that simple enough optimization and control, but rich capture loads. In this work, propose three classes approximate TCL...
Controllers for dynamical systems that operate in safety-critical settings must account stochastic disturbances. Such disturbances are often modeled as process noise a system, and common assumptions the underlying distributions known and/or Gaussian. In practice, however, these may be unrealistic can lead to poor approximations of true distribution. We present novel controller synthesis method does not rely on any explicit representation distributions. particular, we address problem...
We present a constructive procedure for obtaining finite approximate abstraction of discrete-time stochastic hybrid system. The consists partition the state space system and depends on controllable parameter. Given proper continuity assumptions model, approximation errors introduced by are explicitly computed it is shown that they can be tuned through parameter partition. interpreted as Markov set-Chain. show enforcement certain ergodic properties model implies existence with error in time...
FAUST$^2$ is a software tool that generates formal abstractions of (possibly non-deterministic) discrete-time Markov processes (dtMP) defined over uncountable (continuous) state spaces. A dtMP model specified in MATLAB and abstracted as finite-state chain or decision processes. The abstraction procedure runs employs parallel computations fast manipulations based on vector calculus. abstract formally put relationship with the concrete via user-defined maximum threshold approximation error...
This work deals with Markov processes that are defined over an uncountable state space (possibly hybrid) and embedding non-determinism in the shape of a control structure. The contribution looks at problem optimization, set allowed controls, probabilistic specifications by automata - particular, focus is on deterministic finite-state automata. can be reformulated as optimization reachability property product process obtained from model for specification system. Optimizing automata-based thus...
This paper studies the infinite-horizon sensor scheduling problem for linear Gaussian processes with measurement functions. Several important properties of optimal schedules are derived. In particular, it is proved that under some mild conditions, both average-per-stage cost and corresponding independent covariance matrix initial state. It also estimation can be approximated arbitrarily closely by a periodic schedule finite period. Moreover, shown sequence costs must converge. These...