probabilistic model checking on propositional projection temporal logic

	probabilistic model checking on propositional projection temporal logic
	Yang Xiaoxiao
	2011
会议名称	International MultiConference of Engineers and Computer Scientists 2011, IMECS 2011
会议录名称	IMECS 2011 - International MultiConference of Engineers and Computer Scientists 2011
页码	242-248
会议日期	March 16,
会议地点	Kowloon, Hong kong
收录类别	EI
出版地	Hong Kong
ISBN	9789881821034
部门归属	(1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
摘要	Prepositional Projection Temporal Logic (PPTL) is a useful formalism for reasoning about period of time in hardware and software systems and can handle both sequential and parallel compositions. In this paper, based on discrete time Markov chains, we investigate the probabilistic model checking approach for PPTL towards verifying arbitrary linear-time properties. We first define a normal form graph, denoted by NFGinf, to capture the infinite paths of PPTL formulas. Then we present an algorithm to generate the NFG inf. Since discrete-time Markov chains are the deterministic probabilistic models, we further give an algorithm to determinize and minimize the nondeterministic NFGinf following the Safra's construction.
关键词	Algorithms Computer Hardware Computer Science Engineers Markov Processes Probabilistic Logics Temporal Logic
主办者	IAENG Society of Artificial Intelligence; IAENG Society of Bioinformatics; IAENG Society of Computer Science; IAENG Society of Data Mining; IAENG Society of Electrical Engineering
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/14247
专题	基础软件与系统重点实验室
推荐引用方式 GB/T 7714	Yang Xiaoxiao. probabilistic model checking on propositional projection temporal logic[C]. Hong Kong,2011:242-248.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
probabilistic model （682KB）			开放获取	--	请求全文