|
|
|
|
|
|
by fallingmeat
1422 days ago
|
|
|
Have you explored using a formal verification tool to prove out the safety/liveness properties of your (or the end user's) autonomy specifications? Could you model the system in something like Spin/NuSMV/PRISM and then ensure that certain properties hold (useful states are reachable and dangerous ones are not)? |
|
|
No, we haven't looked into formal tools like that, good suggestion! TBD on if these approaches bode well for real world robotics, (due to model complexity and model/real world fit problems) but at least there seems to be some applications to path planning and controls: https://ieeexplore.ieee.org/document/5509686
I'll pass it on to the controls team!