search

mvcisback / magnumSTL

BSD 3-Clause "New" or "Revised" License
0 stars 4 forks source link

Define future research directions #3

Open mvcisback opened 8 years ago

mvcisback commented 8 years ago

Based on previous discussions:

  1. [ ] Support probabilistic/mixed strategies:
    • Mixed strategies guarantee that the input space is convex (since the expectation is a convex combination).
    • They are guaranteed to exist via the NashEq. (in fact this is zero-sum so it's a CCE)
    • Brings us closer to traditional differential games literature.
  2. [ ] "Bloat" strategies/counter-strategies to make measurable progress during CEGIS loop:
    • What does 1 strategy say about neighboring strategies?
    • Under what conditions does the current system loop indefinitely?
    • How do we relate strategies to the robustness of the generated traces? Worst Case/Expectation?
  3. [ ] Investigate using SMT solvers rather than MILP
    • Designed to be incremental (can reuse work done during CEGIS loop).
    • Give conflict lemmas explaining UNSAT conditions.
    • desugared discrete STL' should correspond to theories of Linear Arithmetic.
  4. [ ] Explore smooth quantitative semantics:
    • Candidates are quasi-arithmetic means.
    • May allow on to express as differential game and not require discrete time.