Presentation	2003/5/22 CTL Model cheking with Model Generation Theorem Prover Ryo SHIMIZU, Ryuzo HASEGAWA, Miyuki KOSHIMURA,
PDF Download Page	PDF download Page Link
Abstract(in Japanese)	(See Japanese page)
Abstract(in English)	This paper presents a method performing CTL model checking with a model generation theorem prover. In this method, a transition system and a negation of its specification are represented by a clause set. The model checking is performed by checking satisfiability of the clause set. If the transition system satisfies the specification, the clause set are unsatisfiable, otherwise, it is satisfiable. In the latter, the theorem prover returns a model as a counter example which show a possible error of the transition system.
Keyword(in Japanese)	(See Japanese page)
Keyword(in English)	CTL / model checking / model generation
Paper #	AI2003-7
Date of Issue

Conference Information
Committee	AI
Conference Date	2003/5/22(1days)
Place (in Japanese)	(See Japanese page)
Place (in English)
Topics (in Japanese)	(See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To	Artificial Intelligence and Knowledge-Based Processing (AI)
Language	JPN
Title (in Japanese)	(See Japanese page)
Sub Title (in Japanese)	(See Japanese page)
Title (in English)	CTL Model cheking with Model Generation Theorem Prover
Sub Title (in English)
Keyword(1)	CTL
Keyword(2)	model checking
Keyword(3)	model generation
1st Author's Name	Ryo SHIMIZU
1st Author's Affiliation	Graduate School of Information Science and Electrical Engineering Kyushu Univercity()
2nd Author's Name	Ryuzo HASEGAWA
2nd Author's Affiliation	Graduate School of Information Science and Electrical Engineering Kyushu Univercity
3rd Author's Name	Miyuki KOSHIMURA
3rd Author's Affiliation	Graduate School of Information Science and Electrical Engineering Kyushu Univercity
Date	2003/5/22
Paper #	AI2003-7
Volume (vol)	vol.103
Number (no)	103
Page	pp.pp.-
#Pages	6
Date of Issue