Presentation 2010-03-08
Reachability Analysis for Probabilistic Timed System based on Timed Abstraction Refinement Technique
Akihiko ITO, Takeshi NAGAOKA, Kozo OKANO, Shinji KUSUMOTO,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) This paper gives a reachability analysis technique for Probabilistic Timed Automaton (PTA), based on CEGAR loop. The proposed method uses a transformation technique in order to avoid influence caused by dynamic change of behaviour with elapsing time.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) Timed Probabilistic System / Model Checking / CEGAR / Simulation
Paper # SS2009-62
Date of Issue

Conference Information
Committee SS
Conference Date 2010/3/1(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 Software Science (SS)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Reachability Analysis for Probabilistic Timed System based on Timed Abstraction Refinement Technique
Sub Title (in English)
Keyword(1) Timed Probabilistic System
Keyword(2) Model Checking
Keyword(3) CEGAR
Keyword(4) Simulation
1st Author's Name Akihiko ITO
1st Author's Affiliation Graduate School of Information Science and Technology, Osaka University()
2nd Author's Name Takeshi NAGAOKA
2nd Author's Affiliation Graduate School of Information Science and Technology, Osaka University
3rd Author's Name Kozo OKANO
3rd Author's Affiliation Graduate School of Information Science and Technology, Osaka University
4th Author's Name Shinji KUSUMOTO
4th Author's Affiliation Graduate School of Information Science and Technology, Osaka University
Date 2010-03-08
Paper # SS2009-62
Volume (vol) vol.109
Number (no) 456
Page pp.pp.-
#Pages 6
Date of Issue