## 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.

## 2016年10月6日木曜日

### 2016/10/06

In order to learn DBM that is used in the implementation of Zone Graph, I am reading Timing assumptions and verification of finite-state concurrent systems. This paper is written before A theory of timed automata. Therefore the dense time model was new and the automaton representing the system is a subset of the timed automaton.

## 2016年10月3日月曜日

### 2016/10/03

In the morning, I have attended a class of categories.

These days, I read Analyzing Timed Systems Using Tree Automata to use in my work. Today I tried to understand the tree automata for validity. Since I have almost forgotten tree automata, I also reviewed some properties about tree automata with Wikipedia. In this paper, non-deterministic bottom-up tree automata are used. I also ran the tree automaton by hand. I realized my approach was difficult. I need to think another method.