Art

J-GLOBAL ID：200902284090876023   Reference number：06A0246948

A Method to Generate Formulae for Temporal Logic Satisfiability Checkers

時相論理の充足可能性判定器のための論理式生成法

Author (7)： SEKIZAWA TOSHIFUSA (JST-CREST) ,  SEKIZAWA TOSHIFUSA (産業技術総合研) ,  TAKAI TOSHINORI (JST-CREST) ,  TAKAI TOSHINORI (産業技術総合研) ,  TANABE YOSHINORI (JST-CREST) ,  TANABE YOSHINORI (産業技術総合研) ,  TAKAHASHI KOICHI (産業技術総合研)
Material： 電子情報通信学会論文誌 D  (IEICE Transactions on Information and Systems (Japanese Edition))
Volume： J89-D  Issue： 4  Page： 642-650  Publication year： Apr. 01, 2006 
JST Material Number： S0757C  ISSN： 1880-4535  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： *temporal logic ,...
Semi thesaurus term： 充足可能性判定 ,...

   To see more with JDream III (charged).   {{ this.onShowAbsJLink("http://jdream3.com/lp/jglobal/index.html?docNo=06A0246948&from=J-GLOBAL&jstjournalNo=S0757C") }}

JST classification (1)： Theory of computation  (JB02000A)

Reference (14)：

• P. Balsiger, A. Heuerding, and S. Schwendimann, “A benchmark method for the propositional modal logics K, KT, S4,” J. Automated Reasoning, vol.24, no.3, pp. 297-317, 2000.
• E. M. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, 2000.
• M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, “Paterns in property specifications for finite-state verification,” Proc.21st International Conference on Software Engineering, May 1999.
• E. A. Emerson, “Temporal and modal logic,” in Handbook of Theoretical Computer Science, vol. B, chap. 16, pp. 995-1072, Elsevier and MIT Press, 1990.
• E. A. Emerson and E. M. Clarke, “Using branchingtime temporal logic to-synthesize synchronization skeltons,” Science of Computer Programming, vol.2, no.3, pp. 241-266, 1982.

Terms in the title (3)： 時相論理 ,  充足可能性 ,  論理式