Home
News
People
Publications
Seminar
Courses
Events
Vacancies
Contact
Pulp Fictions
Light
Dark
Automatic
differential dynamics
Derivative-Agnostic Inference of Nonlinear Hybrid Systems
This paper addresses the problem of inferring hybrid automata from input-output traces of hybrid systems exhibiting discrete mode …
Hengzhi Yu
,
Bohan Ma
,
Mingshuai Chen
,
Huangying Dong
,
Jie An
,
Bin Gu
,
Naijun Zhan
,
Jianwei Yin
Cite
Slides
Encoding Inductive Invariants as Barrier Certificates
We present the
invariant barrier-certificate condition
that witnesses unbounded-time safety of differential dynamical systems. The …
Qiuye Wang
,
Mingshuai Chen
,
Bai Xue
,
Naijun Zhan
,
Joost-Pieter Katoen
PDF
Cite
Code
Slides
DOI
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence …
Qiuye Wang
,
Mingshuai Chen
,
Bai Xue
,
Naijun Zhan
,
Joost-Pieter Katoen
PDF
Cite
Slides
Video
DOI
Artifact Evaluated
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety …
Shenghua Feng
,
Mingshuai Chen
,
Bai Xue
,
Sriram Sankaranarayanan
,
Naijun Zhan
PDF
Cite
Slides
Video
DOI
Artifact Evaluated
Pulp Fiction
Taming Delays in Dynamical Systems
Delayed coupling between state variables occurs regularly in technical dynamical systems, especially embedded control. As it …
Shenghua Feng
,
Mingshuai Chen
,
Naijun Zhan
,
Martin Fränzle
,
Bai Xue
PDF
Cite
Slides
DOI
Artifact Evaluated
Verification and Synthesis of Time-Delayed Dynamical Systems
Conventional embedded systems have over the past two decades vividly evolved into an open, interconnected form that integrates …
Mingshuai Chen
Cite
Slides
CAS-President Special Award
In Memory of Oded Maler: Automatic Reachability Analysis of Hybrid-State Automata
Hybrid automata are an elegant formal model seamlessly integrating differential equations representing continuous dynamics with …
Martin Fränzle
,
Mingshuai Chen
,
Paul Kröger
PDF
Cite
DOI
Reachability Analysis for Solvable Dynamical Systems
The reachability problem is one of the most important issues in the verification of hybrid systems. But unfortunately the reachable …
Ting Gan
,
Mingshuai Chen
,
Yangjia Li
,
Bican Xia
,
Naijun Zhan
PDF
Cite
Code
DOI
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations
Delays in feedback control loop, as induced by networked distributed control schemes, may have detrimental effects on control …
Bai Xue
,
Peter Nazier Mosaad
,
Martin Fränzle
,
Mingshuai Chen
,
Yangjia Li
,
Naijun Zhan
PDF
Cite
Slides
Video
DOI
MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems
We introduce a toolchain MARS for Modelling, Analyzing and veRifying hybrid Systems we developed in the past years. Using MARS, we …
Mingshuai Chen
,
Xiao Han
,
Tao Tang
,
Shuling Wang
,
Mengfei Yang
,
Naijun Zhan
,
Hengjun Zhao
,
Liang Zou
PDF
Cite
Code
DOI
»
Cite
×