Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userEfficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems
625
0
0.0
(
0
)
Added by
Nathalie Cauchi
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process (IMDP). Then, a strategy that maximizes the satisfaction probability of the given specification is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, which are by and large limited to finite-time properties and rely on conservative over-approximations, we show that the exact abstraction error can be computed as a solution of convex optimization problems and can be embedded into the IMDP abstraction. This is later used in the synthesis step over both finite- and infinite-horizon specifications, mitigating the known state-space explosion problem. Our experimental validation of the new approach compared to existing abstraction-based approaches shows: (i) significant (orders of magnitude) reduction of the abstraction error; (ii) marked speed-ups; and (iii) boosted scalability, allowing in particular to verify models with more than 10 continuous variables.
rate research
Read More
We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particular, we consider hybrid systems with nonlinear dynamics (Lipschitz-continuous ordinary differential equations) and random parameters, and we synthesize PID controllers such that the resulting closed-loop systems satisfy safety and performance constraints given as probabilistic bounded reachability properties. Our technique leverages SMT solvers over the reals and nonlinear differential equations to provide formal guarantees that the synthesized controllers satisfy such properties. These controllers are also robust by design since they minimize the probability of reaching an unsafe state in the presence of random disturbances. We apply our approach to the problem of insulin regulation for type 1 diabetes, synthesizing controllers with robust responses to large random meal disturbances, thereby enabling them to maintain blood glucose levels within healthy, safe ranges.
Stochastic HYPE is a novel process algebra that models stochastic, instantaneous and continuous behaviour. It develops the flow-based approach of the hybrid process algebra HYPE by replacing non-urgent events with events with exponentially-distributed durations and also introduces random resets. The random resets allow for general stochasticity, and in particular allow for the use of event durations drawn from distributions other than the exponential distribution. To account for stochasticity, the semantics of stochastic HYPE target piecewise deterministic Markov processes (PDMPs), via intermediate transition-driven stochastic hybrid automata (TDSHA) in contrast to the hybrid automata used as semantic target for HYPE. Stochastic HYPE models have a specific structure where the controller of a system is separate from the continuous aspect of this system providing separation of concerns and supporting reasoning. A novel equivalence is defined which captures when two models have the same stochastic behaviour (as in stochastic bisimulation), instantaneous behaviour (as in classical bisimulation) and continuous behaviour. These techniques are illustrated via an assembly line example.
We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitalization of signals by the controller. Our approach has two stages, leveraging counterexample guided inductive synthesis (CEGIS) and reachability analysis. CEGIS synthesizes a static feedback controller that stabilizes the system under restrictions given by the safety of the reach space. Safety is verified either via BMC or abstract acceleration; if the verification step fails, we refine the controller by generalizing the counterexample. We synthesize stable and safe controllers for intricate physical plant models from the digital control literature.
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 is specified in MATLAB and abstracted as a finite-state Markov chain or Markov decision processes. The abstraction procedure runs in MATLAB and employs parallel computations and fast manipulations based on vector calculus. The abstract model is formally put in relationship with the concrete dtMP via a user-defined maximum threshold on the approximation error introduced by the abstraction procedure. FAUST$^2$ allows exporting the abstract model to well-known probabilistic model checkers, such as PRISM or MRMC. Alternatively, it can handle internally the computation of PCTL properties (e.g. safety or reach-avoid) over the abstract model, and refine the outcomes over the concrete dtMP via a quantified error that depends on the abstraction procedure and the given formula. The toolbox is available at http://sourceforge.net/projects/faust2/
We develop a compositional framework for formal synthesis of hybrid systems using the language of category theory. More specifically, we provide mutually compatible tools for hierarchical, sequential, and independent parallel composition. In our framework, hierarchies of hybrid systems correspond to template-anchor pairs, which we model as spans of subdividing and embedding semiconjugacies. Hierarchical composition of template-anchor pairs corresponds to the composition of spans via pullback. To model sequential composition, we introduce directed hybrid systems, each of which flows from an initial subsystem to a final subsystem in a Conley-theoretic sense. Sequential composition of directed systems is given by a pushout of graph embeddings, rewriting the continuous dynamics of the overlapping subsystem to prioritize the second directed system. Independent parallel composition corresponds to a categorical product with respect to semiconjugacy. To formalize the compatibility of these three types of composition, we construct a vertically cartesian double category of hybrid systems where the vertical morphisms are semiconjugacies, and the horizontal morphisms are directed hybrid systems.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
