| タイトル | Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae |
| 本文（外部サイト） | http://hdl.handle.net/2060/20010106096 |
| 著者（英） | Havelund, Klaus; Rosu, Grigore |
| 著者所属（英） | Research Inst. for Advanced Computer Science |
| 発行日 | 2001-01-01 |
| 言語 | eng |
| 内容記述 | The problem of testing a linear temporal logic (LTL) formula on a finite execution trace of events, generated by an executing program, occurs naturally in runtime analysis of software. We present an algorithm which takes an LTL formula and generates an efficient dynamic programming algorithm. The generated algorithm tests whether the LTL formula is satisfied by a finite trace of events given as input. The generated algorithm runs in linear time, its constant depending on the size of the LTL formula. The memory needed is constant, also depending on the size of the formula. |
| NASA分類 | Computer Programming and Software |
| 権利 | No Copyright |
| URI | https://repository.exst.jaxa.jp/dspace/handle/a-is/225731 |
