tag:blogger.com,1999:blog-75221615097477870772017-07-17T22:14:55.033+09:00Masaki's research dialyMasaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.comBlogger11125tag:blogger.com,1999:blog-7522161509747787077.post-45994677526949761132017-02-27T19:39:00.000+09:002017-02-27T19:39:41.669+09:002017/02/27<p>These days I survey on SLA monitoring. The approach in <a href="http://dl.acm.org/citation.cfm?id=1453125">Efficient online monitoring of web-service SLAs</a> 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. </p> <p>Today, I am reading a survey <a href="http://www.optimis-project.eu/sites/default/files/content-files/document/analysis-existing-solutions-requirements-slas.pdf">Analysis of Existing solutions and Requirements for SLAs</a>. In this paper, 5 languages are described: SLAng; WS-Agreement; WSLA; WSOL; and SWAPS. <a href="https://de.wikipedia.org/wiki/WS-Agreement">WS-Agreement</a> seems to be a good option. </p> <p><a href="http://gessi.lsi.upc.edu/salmon/web/">SALMon</a> is a monitoring tool of SLA. However, when we use more high level tools like <a href="https://www.icinga.com/">icinga</a> seems to be better. </p> <p>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. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-76911381328978507532016-10-07T17:31:00.001+09:002016-10-07T17:31:22.121+09:002016/10/07<p>I continued reading <a href="http://link.springer.com/chapter/10.1007%2F3-540-52148-8_17#page-1">Timing assumptions and verification of finite-state concurrent systems</a> 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. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-71052416121016269832016-10-06T19:21:00.000+09:002016-10-06T19:21:31.940+09:002016/10/06<p>In order to learn DBM that is used in the implementation of Zone Graph, I am reading <a href="http://link.springer.com/chapter/10.1007%2F3-540-52148-8_17#page-1">Timing assumptions and verification of finite-state concurrent systems</a>. This paper is written before <a href="http://www.cis.upenn.edu/~alur/TCS94.pdf">A theory of timed automata</a>. Therefore the dense time model was new and the automaton representing the system is a subset of the timed automaton. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-4619735552606912642016-10-03T16:58:00.001+09:002016-10-03T16:58:58.096+09:002016/10/03<p>In the morning, I have attended a class of categories. </p> <p>These days, I read <a href="https://arxiv.org/abs/1604.08443">Analyzing Timed Systems Using Tree Automata</a> 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 <a href="https://en.wikipedia.org/wiki/Tree_automaton">Wikipedia</a>. 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. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-34156652203009361912016-07-06T10:54:00.003+09:002016-10-04T14:33:45.140+09:00References<dl><dt>Zone Automata</dt><dd><a href="http://dl.acm.org/citation.cfm?id=1507245">Checking timed Büchi automata emptiness on simulation graphs</a></dd><dt>Tree Automata</dt><dd><a href="https://www8.cs.umu.se/kurser/5DV023/VT09/final.pdf">Lecture notes on TREE AUTOMATA</a></dd></dl>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-32268021889966522072016-07-05T11:42:00.004+09:002016-07-05T11:42:34.706+09:002016/07/05<p>I have read the preliminary part of <a href="http://www.lsv.ens-cachan.fr/Projects/anr-dots/PUBLIS/HSW-cav10.pdf">Efficient Emptiness Check for Timed Büchi Automata</a> 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. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-60346493124533631382016-06-15T19:54:00.003+09:002016-10-03T14:19:07.846+09:002016/06/15<p>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 "<a href="http://www.fi.muni.cz/~xpelanek/IA158/TA-intro.pdf">Timed Automata: Semantics, Algorithms and Tools</a>". Now I am not sure if zone automata are applicable to my work. I have to survey more. </p> <p>I attended to Quantitative Seminar in our laboratory. We read <a href="http://www.sciencedirect.com/science/article/pii/S0022000011000511">survey paper of Stochastic games</a>. </p> <p>I attended a class of reversible computing. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-25673383350855605302016-06-13T17:34:00.002+09:002016-06-13T17:34:39.539+09:002016/06/13<p>Form the last weekend, I am reading <a href="http://www.sciencedirect.com/science/article/pii/S0012365X06004225">Totally anti-symmetric quasigroups for all orders n≠2,6</a> and <a href="http://link.springer.com/article/10.1007/s000130050524">Check digit systems over groups and anti-symmetric mappings</a> to write a report. I realized the method in <a href="https://en.wikipedia.org/wiki/Damm_algorithm">Wikipedia</a> is different from the original one. I confused by this. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-70509551178673388842016-06-10T22:21:00.000+09:002016-06-10T22:21:47.294+09:002016/06/10<p>Today I attended a class of matrix. Today it was about Graph. </p><p>I wrote about half of the report about reversible computing. </p><p>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. </p><p>I found some paper about hybrid games, that can be applied to controller synthesis. <ul><li> http://digitalassets.lib.berkeley.edu/techreports/ucb/text/CSD-99-1044.pdf <li> http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf <li> http://people.cis.ksu.edu/~pprabhakar/papers/2009/hscc09/hscc09.pdf </ul></p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-42747908779562688832016-06-06T21:09:00.001+09:002016-06-06T21:09:38.602+09:002016/06/06<p>These days, I read <a href="http://www.sciencedirect.com/science/article/pii/S0304397515009792">Modelling and verification of weighted spiking neural systems</a>. 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. </p> <p>About two weeks ago, I have read almost all of the <a href="http://software.imdea.org/es/people/pavithra.prabhakar/papers/2008/icalp08/icalp08.pdf">STORMED hybrid systems</a> 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 <a href="https://www.researchgate.net/profile/Pavithra_Prabhakar/publication/220897822_STORMED_Hybrid_Systems/links/55033dd50cf231de076fe395.pdf">slide</a>. I will read this later. </p> <p>This is the largest work of today. I have written <a href="http://maswag-gcl.tumblr.com/post/145499753182/social-issues-and-the-research">an article</a> about Social Issue and Research. It was very hard because it had to be 400-600 words, that is very long. </p> <p>I also tried to understand <a href="https://en.wikipedia.org/wiki/Damm_algorithm">Damm algorithm</a> but I could only understand quasi group and totally anti-symmetricity because I was too tired. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0tag:blogger.com,1999:blog-7522161509747787077.post-45329041993902861822016-05-30T17:55:00.000+09:002016-06-02T14:50:58.106+09:002016/05/30<p>Today I have read some part of <a href="http://www.control.lth.se/media/Education/EngineeringProgram/FRTN05/2015/lec04_2015eight.pdf">Lyapunov Stability</a> 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 <a href="http://vmahesh.cs.illinois.edu/papers/icalp08.pdf">STORMED hybrid systems</a> is closely related to Lyapunov function. </p>Masaki Wagahttp://www.blogger.com/profile/10691663625887810294noreply@blogger.com0