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

2016年6月13日月曜日

2016年6月10日金曜日

2016/06/10

Today I attended a class of matrix. Today it was about Graph.

I wrote about half of the report about reversible computing.

I discussed approximate bisimulation. I have read a survey paper with some example application. My colleague read a paper about a stocastic extension of approximate bisimulation. It can treat brown noise.

I found some paper about hybrid games, that can be applied to controller synthesis.

  • http://digitalassets.lib.berkeley.edu/techreports/ucb/text/CSD-99-1044.pdf
  • http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf
  • http://people.cis.ksu.edu/~pprabhakar/papers/2009/hscc09/hscc09.pdf

2016年6月6日月曜日

2016/06/06

These days, I read Modelling and verification of weighted spiking neural systems. Today, I read the latter part of Section 4 (Relating spiking neural P systems to timed safety automata). Here, the construction of the safety timed automaton from a spiking neural P system is presented. The bisimulation relation between spiking neural P systems and safety timed automata is defined and the main theorem, that is the constructed safety timed automaton is bisimilar to the given spiking neural P system.

About two weeks ago, I have read almost all of the STORMED hybrid systems except the Section 6 (Relaxations of the STORMED model). I tried to read it but I have not read the proof. I also found the slide. I will read this later.

This is the largest work of today. I have written an article about Social Issue and Research. It was very hard because it had to be 400-600 words, that is very long.

I also tried to understand Damm algorithm but I could only understand quasi group and totally anti-symmetricity because I was too tired.

2016年5月30日月曜日

2016/05/30

Today I have read some part of Lyapunov Stability to learn Lyapunov function, that seems useful for reading http://www.sciencedirect.com/science/article/pii/S0947358011709773. Lyapunov function is a function that has the following energy-like properties: its value is 0 at the equilibrium point; its value is positive at any point except equilibrium point; and its value does not increase along all trajectories of the system. By Lyapunov theorem, if there exists a Lyapunov function, the equilibrium point is locally stable, that is a trajectory is "near" from the equilibrium point (the threshold of "near" can be defined arbitrarily) when the start point is enough near from the equilibrium point. I think the Monotonicity property in STORMED hybrid systems is closely related to Lyapunov function.