Presentation 1999/1/23
Model checking for communicating processes by the context transformation method
Yasuo Kikawa, Shoji Yuen, Toshiki Sakabe,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) In this paper, we present a model checking method with decomposition for communicating processes characterized by the weak version of Hennessy-Milner Logic formulas. We transform a characterizing formula according to a context constructed by the composition operator so that the formula is valid in environment specified by the context. By the context transformation, we can decompose a communicating process to some sub-processes and perform model checking for a certain sub-process. Using our method for a local property, we can efficiently establish a model checking proof by pruning unnecessary proofs. Finally, we illustrate the usefulness of our context transformation method by an example.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) Communicating processes / Model checking
Paper # COMP98-82
Date of Issue

Conference Information
Committee COMP
Conference Date 1999/1/23(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 Theoretical Foundations of Computing (COMP)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Model checking for communicating processes by the context transformation method
Sub Title (in English)
Keyword(1) Communicating processes
Keyword(2) Model checking
1st Author's Name Yasuo Kikawa
1st Author's Affiliation Graduate School of Engineering, Nagoya University()
2nd Author's Name Shoji Yuen
2nd Author's Affiliation Center for Information Media Studies, Nagoya University
3rd Author's Name Toshiki Sakabe
3rd Author's Affiliation Graduate School of Engineering, Nagoya University
Date 1999/1/23
Paper # COMP98-82
Volume (vol) vol.98
Number (no) 562
Page pp.pp.-
#Pages 8
Date of Issue