search

AutoVerse-ai / Verse-library

Library for modeling, simulation, and verification of interacting autonomous agents
https://autoverse-ai.github.io/Verse-library/
University of Illinois/NCSA Open Source License
29 stars 18 forks source link

Reachtube computations with diffrent \delta values are not refinements. #27

Closed sayanmitracode closed 1 year ago

sayanmitracode commented 1 year ago

When we compute reachtubes of the same model with different \delta-values then Reach(X_0,\delta_1) is expected to be a subset of Reach(X_0, delta_2) provided delta_2 < delta_1. This appears to be not the case sometimes. To see this run python3 demo/AEB/exp2_curve.py with different time parameters 0.1 and 1.

lyg1597 commented 1 year ago

I looked into this example and the behavior kind of match what we expected. Since $\delta=1$ causes more over-approximations, it triggers a safety violation before the transition can complete and therefore causes verification to stop immediately. That's why the transition doesn't happen. To solve this, we may want to find a tighter way for us to handle guard and reset in the tool or maybe change how we are processing safety assertions.

crides commented 1 year ago

We do currently have the unsafe_continue option in ScenarioConfig to allow the reachability algorithm to continue when an assertion/unsafe condition is hit

sayanmitracode commented 1 year ago

I see. This sequence of examples is a good one to have in our presentation / demo / notebooks, illustrating these points we have discussed in the thread. Otherwise, let us move on to the next item. Seeing lots of commits; I assume one of you will let me know when the code, documentation are ready for me to take a look.

Sayan

From: lyg1597 @.> Date: Wednesday, May 24, 2023 at 04:18 To: AutoVerse-ai/Verse-library @.> Cc: sayan m @.>, Author @.> Subject: Re: [AutoVerse-ai/Verse-library] Reachtube computations with diffrent delta values are not refinements. (Issue #27)

I looked into this example and the behavior kind of match what we expected. Since $\delta=1$ causes more over-approximations, it triggers a safety violation before the transition can complete and therefore causes verification to stop immediately. That's why the transition doesn't happen. To solve this, we may want to find a tighter way for us to handle guard and reset in the tool or maybe change how we are processing safety assertions.

— Reply to this email directly, view it on GitHubhttps://github.com/AutoVerse-ai/Verse-library/issues/27#issuecomment-1560365248, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ACR7QWETFX6KH6D5A52YZR3XHVVWFANCNFSM6AAAAAAYLTG67E. You are receiving this because you authored the thread.Message ID: @.***>

sayanmitracode commented 1 year ago

The above explanation makes sense.