Weekly Meeting Aug 29, 2020

Winstead via FLUENT Verification Project

Fri, 30 Oct 2020 16:30:59 -0600

!FLUENT Verification Project

Attending: Chris W, Zhen, Lukas, Tom, Laureano, Mohammad, Nisa, Payton, Riley

Agenda

Chris W -- making progress with Tom, moving onto MC integration for state machines and Markov models. Zhen will try and recruit another REU student since Darren is out this semester. Chris W will see if Darren is interested in rejoining during spring.
Lukas is working on a paper; will get contributions from Zhen and Riley
Payton -- status of reb2sac in docker looks promising, not done yet. Java code is Dockerized.
Mohammad -- fixed a bug that shows wrong probabilities in subgraphs
Nisa -- running new models with bounded model checking on DTMC, moving code around
Laureano -- almost ready to implement IC3, still studying T3
Riley -- Doing heuristic exploration to iteratively change reachability rather than recursively. Starts with a kappa of 1, then divides kappa by 2 in subsequent iterations. Similar to parametric optimization frameworks? Homotopy methods?

#meetings

meetings

Winstead

Fri, 30 Oct 2020 16:37:32 -0600

@Riley Roberts what you're doing probably fits into a subclass of iterative methods, of which there are many. A particularly exotic example is the homotopy method, which takes a hard problem and "distorts" it into an easy problem. Then, by small increments, the easy problem is deformed back into the hard problem in such a way that each incremental step converges when using information from the previous step.

Zhen Zhang

Fri, 30 Oct 2020 20:56:48 -0600

@Winstead Thanks, Chris. I asked Riley to formulate an algorithm for the improvement he made. I think it will help us to see more clearly on how it fits the homotopy method.