QQ客服 官方微博 反馈留言

	Satisfiability of Linear Time Mu-Calculus on Finite Traces
	Liu, Yao ; Duan, Zhenhua ; Tian, Cong ; Cui, Bin
	2016
关键词	Linear time mu-calculus Finite traces Present future form graph Decision procedure Satisfiability TEMPORALLY EXTENDED GOALS LOGIC
英文摘要	In this paper, we study linear time mu-calculus interpreted over finite traces, namely nu TLf. We define Present Future form (PF form) for nu TLf formulas and prove that every closed nu TLf formula can be converted into this form. PF form decomposes a formula into two parts: what to be satisfied at the current state and what to be satisfied at the next one. Based on PF form, we provide an algorithm for constructing Present Future form Graph (PFG) that can be employed to depict models of a formula. In addition, a decision procedure for checking satisfiability of nu TLf formulas based on PFG is proposed.; EI; CPCI-S(ISTP); yao_liu@stu.xidian.edu.cn; zhhduan@mail.xidian.edu.cn; ctian@mail.xidian.edu.cn; bin.cui@pku.edu.cn; 611-622; 9797
语种	英语
出处	22nd International Computing and Combinatorics Conference (COCOON)
DOI标识	10.1007/978-3-319-42634-1_49
内容类型	其他
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/449581]
专题	信息科学技术学院
推荐引用方式 GB/T 7714	Liu, Yao,Duan, Zhenhua,Tian, Cong,et al. Satisfiability of Linear Time Mu-Calculus on Finite Traces. 2016-01-01.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。