Presentation	2002/10/11 A SAT-based Model Checking Method for Asynchronous Concurrent Systems Tatsuhiro TSUCHIYA, Tohru KIKUNO,
PDF Download Page	PDF download Page Link
Abstract(in Japanese)	(See Japanese page)
Abstract(in English)	Bounded model checking has received recent attention as an efficient verification method. The basic idea of this method is to reduce the model checking problem to the propositional satisfiability (SAT) decision problem. For asynchronous systems, however, this method does not work well because the resulting propositional formulastend to become very large for such systems. In this paper, we take 1-bounded Petri nets as a plausible model of asynchronous systems and propose an alternative encoding method for them. This method is simple but can generate very succinct formulas, thus resulting in reduced verification times.
Keyword(in Japanese)	(See Japanese page)
Keyword(in English)	Model checking / SAT / asynchronous system / Petri net
Paper #	DE2002-95
Date of Issue

Conference Information
Committee	DE
Conference Date	2002/10/11(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	Data Engineering (DE)
Language	ENG
Title (in Japanese)	(See Japanese page)
Sub Title (in Japanese)	(See Japanese page)
Title (in English)	A SAT-based Model Checking Method for Asynchronous Concurrent Systems
Sub Title (in English)
Keyword(1)	Model checking
Keyword(2)	SAT
Keyword(3)	asynchronous system
Keyword(4)	Petri net
1st Author's Name	Tatsuhiro TSUCHIYA
1st Author's Affiliation	Graduate School of Information Science and Technology, Osaka University()
2nd Author's Name	Tohru KIKUNO
2nd Author's Affiliation	Graduate School of Information Science and Technology, Osaka University
Date	2002/10/11
Paper #	DE2002-95
Volume (vol)	vol.102
Number (no)	376
Page	pp.pp.-
#Pages	6
Date of Issue