REVIEW 5 cited by
Data-driven Abstractions for Verification of Deterministic Systems
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
abstract
A common technique to verify complex logic specifications for dynamical systems is the construction of symbolic abstractions: simpler, finite-state models whose behaviour mimics the one of the systems of interest. Typically, abstractions are constructed exploiting an accurate knowledge of the underlying model: in real-life applications, this may be a costly assumption. By sampling random $\ell$-step trajectories of an unknown system, we build an abstraction based on the notion of $\ell$-completeness. We newly define the notion of probabilistic behavioural inclusion, and provide probably approximately correct (PAC) guarantees that this abstraction includes all behaviours of the concrete system, for finite and infinite time horizon, leveraging the scenario theory for non convex problems. Our method is then tested on several numerical benchmarks.
Forward citations
Cited by 5 Pith papers
-
Reinforcement Learning for Robust Ageing-Aware Control of Li-ion Battery Systems with Data-Driven Formal Verification
An RL-based charging controller for Li-ion batteries, refined via counterexample-guided synthesis, is verified with a data-driven abstraction to satisfy a reach-while-avoid specification with probability at least 99.956%.
-
Temporal Logic Control for Nonlinear Stochastic Systems Under Unknown Disturbances
A data-driven abstraction framework using two-layer state discretization and learned disturbance support synthesizes robust temporal-logic strategies for nonlinear stochastic systems with unknown noise.
-
Abstraction-based Control of Unknown Continuous-Space Models with Just Two Trajectories
A two-trajectory data-driven method constructs a symbolic abstraction and a formal alternating simulation certificate, enabling controller refinement for unknown polynomial systems.
-
A Pragmatic Guide to Building Conservative Discrete Abstractions of Cyber-Physical Systems
This paper is a tutorial on building conservative discrete abstractions for verification of cyber-physical systems, but its proposed self-loop erasure technique can under-approximate the true one-step transitions.
-
Data-Driven Formal Methods for Complex Dynamical Systems: A Survey
A taxonomy and survey of data-driven formal verification and controller synthesis, organized around abstraction-based, functional-certificate, and compositional methods with PAC, Lipschitz, and structural-property guarantees.
Discussion (0). Continue with ORCID to comment.