## 2016年10月7日金曜日

### 2016/10/07

I continued reading Timing assumptions and verification of finite-state concurrent systems to learn BDM. BDM is a matrix that can represent a zone. A BDM represents constraints $x_i - x_j \le d_{i,j}$ where $x_0 = 0$. A zone can be represented more than one zone but we can calculate minimum constraint with Warshall-Froyd algorithm.