Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation

Mikkel Bjørn, Daniel H. Hansen, Grace Melchiors, Kim Guldstrand Larsen, Christian Schilling

arXivarxiv/2606.26352Jun 24, 2026eess.SYscore 0

We study safety verification for linear time-invariant systems with bounded inputs in continuous time. The standard approach reduces to a reachability analysis in two steps: first discretize time and then apply a forward analysis in the discretized system. Existing algorithms use either a fixed time step or an adaptive time step that changes based on the approximation error compared to the underlying continuous system. In this paper, we present an efficient reachability algorithm that adapts the time step based on a given safety property. Essentially, our algorithm makes the largest possible…

SourceJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2606.26352
curl -X POST /api/v1/records/arxiv/2606.26352/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2606.26352/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'