Modelling Relaxed Accesses

Work at IIT Bombay and Uppsala University, Sweden under guidance of Profs. Krishna S., Parosh Abdulla and Faouzi Atig

Verification of programs

• The control state reachability problem asks, a concurrent program $\mathcal{P}$ under a particular memory model, with processes, ,$p_1$, $p_2$, ..., $p_k$, is the control state $(\lambda_1, \lambda_2, \cdots, \lambda_k)$ reachable?

Possible Future Work

Probabilistic extensions of these systems - MDPs- may be used to model agents

NFAs are polynomial-time synchronizable. An interesting problem is to identify MDPs which are sub-polynomial - polylog-time synchronizable