## 2017年2月27日月曜日

### 2017/02/27

These days I survey on SLA monitoring. The approach in Efficient online monitoring of web-service SLAs seems to be an application of our algorithm. Unfortunately, the development speed of SLAng is really slow now and I want to find alternative specification language and show that can be translated into some timed automata.

Today, I am reading a survey Analysis of Existing solutions and Requirements for SLAs. In this paper, 5 languages are described: SLAng; WS-Agreement; WSLA; WSOL; and SWAPS. WS-Agreement seems to be a good option.

SALMon is a monitoring tool of SLA. However, when we use more high level tools like icinga seems to be better.

This area is really complicated and if I want to use our algorithm to this area, we need a specialist of this area or we have to be a specialist.

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

## 2016年7月6日水曜日

### References

Zone Automata
Checking timed Büchi automata emptiness on simulation graphs
Tree Automata
Lecture notes on TREE AUTOMATA

## 2016年7月5日火曜日

### 2016/07/05

I have read the preliminary part of Efficient Emptiness Check for Timed Büchi Automata to learn more about Zone Automata. It says the property in the region automata in [Alur Dill '94] have pre-stability and the zone automata have post-stability. This difference does not matter when checking emptiness but I am not sure if it is critical when applying to my work.

## 2016年6月15日水曜日

### 2016/06/15

I have received notification of FORMATS yesterday. My paper was accepted but I was suggested to use zone automata instead of region automata. I have read some part of "Timed Automata: Semantics, Algorithms and Tools". Now I am not sure if zone automata are applicable to my work. I have to survey more.

I attended to Quantitative Seminar in our laboratory. We read survey paper of Stochastic games.

I attended a class of reversible computing.