on model construction for modal mu-calculus

ISCAS OpenIR

	on model construction for modal mu-calculus
	Qu Nan
	2012
会议名称	IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012
会议录名称	Proceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012
页码	257-260
会议日期	July 4, 2012 - July 6, 2012
会议地点	Beijing, China
收录类别	EI
ISBN	9780769547510
部门归属	(1) Institute of Software Chinese Academy of Sciences Graduate School of Chinese Academy of Sciences P.O.Box 8718 100190 Beijing China
摘要	This paper presents a tableau system for checking satisfiability of modal μ-calculus formulas. When a formula F is satisfiable, a model with size bounded by 2^\|F\| can be extracted from the tableau. We also show that the asymptotic lower bound for the model size of formulas is greater than any polynomial function of the size of formulas. © 2012 IEEE.; This paper presents a tableau system for checking satisfiability of modal μ-calculus formulas. When a formula F is satisfiable, a model with size bounded by 2^\|F\| can be extracted from the tableau. We also show that the asymptotic lower bound for the model size of formulas is greater than any polynomial function of the size of formulas. © 2012 IEEE.
关键词	Formal Logic Software Engineering
主办者	IFIP; Beijing University of Technology
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15794
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Qu Nan. on model construction for modal mu-calculus[C],2012:257-260.