Deciding probabilistic automata weak bisimulation: theory and practice

ISCAS OpenIR

	Deciding probabilistic automata weak bisimulation: theory and practice
	Fioriti, LMF; Hashemi, V; Hermanns, H; Turrini, A
	2016
发表期刊	FORMAL ASPECTS OF COMPUTING
ISSN	0934-5043
卷号	28 期号:1 页码:109-143
摘要	Weak probabilistic bisimulation on probabilistic automata can be decided by an algorithm that needs to check a polynomial number of linear programming problems encoding weak transitions. It is hence of polynomial complexity. This paper discusses the specific complexity class of the weak probabilistic bisimulation problem, and it considers several practical algorithms and linear programming problem transformations that enable an efficient solution. We then discuss two different implementations of a probabilistic automata weak probabilistic bisimulation minimizer, one of them employing SAT modulo linear arithmetic as the solver technology. Empirical results demonstrate the effectiveness of the minimization approach on standard benchmarks, also highlighting the benefits of compositional minimization.; Weak probabilistic bisimulation on probabilistic automata can be decided by an algorithm that needs to check a polynomial number of linear programming problems encoding weak transitions. It is hence of polynomial complexity. This paper discusses the specific complexity class of the weak probabilistic bisimulation problem, and it considers several practical algorithms and linear programming problem transformations that enable an efficient solution. We then discuss two different implementations of a probabilistic automata weak probabilistic bisimulation minimizer, one of them employing SAT modulo linear arithmetic as the solver technology. Empirical results demonstrate the effectiveness of the minimization approach on standard benchmarks, also highlighting the benefits of compositional minimization.
收录类别	SCI
关键词	Complexity Compositional Analysis Concurrency Efficiency Linear Programming Probabilistic Automata Satisfiability Modulo Theories Weak Bisimulation
部门归属	Univ Saarland, Dept Comp Sci, D-66123 Saarbrucken, Germany. Max Planck Inst Informat, D-66123 Saarbrucken, Germany. Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China.
语种	英语
WOS记录号	WOS:000372262000006
引用统计	被引频次：9[WOS] [WOS记录] [WOS相关记录]
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/17348
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Fioriti, LMF,Hashemi, V,Hermanns, H,et al. Deciding probabilistic automata weak bisimulation: theory and practice[J]. FORMAL ASPECTS OF COMPUTING,2016,28(1):109-143.
APA	Fioriti, LMF,Hashemi, V,Hermanns, H,&Turrini, A.(2016).Deciding probabilistic automata weak bisimulation: theory and practice.FORMAL ASPECTS OF COMPUTING,28(1),109-143.
MLA	Fioriti, LMF,et al."Deciding probabilistic automata weak bisimulation: theory and practice".FORMAL ASPECTS OF COMPUTING 28.1(2016):109-143.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
art%3A10.1007%2Fs001（2164KB）			开放获取	使用许可	请求全文