Probabilistic model checking has been widely applied to quantitative analysis of stochastic systems, e.g., analyzing the performance, reliability and survivability of computer and communication systems. In this paper,...Probabilistic model checking has been widely applied to quantitative analysis of stochastic systems, e.g., analyzing the performance, reliability and survivability of computer and communication systems. In this paper, we extend the application of probabilistic model checking to the vehicle to vehicle(V2V) networks. We first develop a continuous-time Markov chain(CTMC) model for the considered V2V network, after that, the PRISM language is adopted to describe the CTMC model, and continuous-time stochastic logic is used to describe the objective survivability properties. In the analysis, two typical failures are considered, namely the node failure and the link failure, respectively induced by external malicious attacks on a target V2V node, and interrupt in a communication link. Considering these failures, their impacts on the network survivability are demonstrated. It is shown that with increasing failure strength, the network survivability is reduced. On the other hand, the network survivability can be improved with increasing repair rate. The proposed probabilistic model checking-based approach can be effectively used in survivability analysis for the V2V networks, moreover, it is anticipated that the approach can be conveniently extended to other networks.展开更多
In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the...In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the electricity price at each time. A PBN is widely used as a model of complex systems, and is appropriate as a model of real-time pricing systems. Using the PBN-based model, real-time pricing systems can be quantitatively analyzed. In this paper, we propose a verification method of real-time pricing systems using the PBN-based model and the probabilistic model checker PRISM. First, the PBN-based model is derived. Next, the reachability problem, which is one of the typical verification problems, is formulated, and a solution method is derived. Finally, the effectiveness of the proposed method is presented by a numerical example.展开更多
In multiagent systems,agents usually do not have complete information of the whole system,which makes the analysis of such systems hard.The incompleteness of information is normally modelled by means of accessibility ...In multiagent systems,agents usually do not have complete information of the whole system,which makes the analysis of such systems hard.The incompleteness of information is normally modelled by means of accessibility relations,and the schedulers consistent with such relations are called uniform.In this paper,we consider probabilistic multiagent systems with accessibility relations and focus on the model checking problem with respect to the probabilistic epistemic temporal logic,which can specify both temporal and epistemic properties.However,the problem is undecidable in general.We show that it becomes decidable when restricted to memoryless uniform schedulers.Then,we present two algorithms for this case:one reduces the model checking problem into a mixed integer non-linear programming(MINLP)problem,which can then be solved by Satisfiability Modulo Theories(SMT)solvers,and the other is an approximate algorithm based on the upper confidence bounds applied to trees(UCT)algorithm,which can return a result whenever queried.These algorithms have been implemented in an existing model checker and then validated on experiments.The experimental results show the efficiency and extendability of these algorithms,and the algorithm based on UCT outperforms the one based on MINLP in most cases.展开更多
It is attractive to formulate problems in computer vision and related fields in term of probabilis- tic estimation where the probability models are defined over graphs, such as grammars. The graphical struc- tures, an...It is attractive to formulate problems in computer vision and related fields in term of probabilis- tic estimation where the probability models are defined over graphs, such as grammars. The graphical struc- tures, and the state variables defined over them, give a rich knowledge representation which can describe the complex structures of objects and images. The proba- bility distributions defined over the graphs capture the statistical variability of these structures. These proba- bility models can be learnt from training data with lim- ited amounts of supervision. But learning these models suffers from the difficulty of evaluating the normaliza- tion constant, or partition function, of the probability distributions which can be extremely computationally demanding. This paper shows that by placing bounds on the normalization constant we can obtain compu- rationally tractable approximations. Surprisingly, for certain choices of loss functions, we obtain many of the standard max-margin criteria used in support vector machines （SVMs） and hence we reduce the learning to standard machine learning methods. We show that many machine learning methods can be obtained in this way as approximations to probabilistic methods including multi-class max-margin, ordinal regression, max-margin Markov networks and parsers, multiple- instance learning, and latent SVM. We illustrate this work by computer vision applications including image labeling, object detection and localization, and motion estimation. We speculate that rained by using better bounds better results can be ob- and approximations.展开更多
随着大数据技术的快速发展,推荐系统成为大数据领域里的一个重要的研究方向.随着基于位置社交网络(Location-Based Social Networks,LBSN)的快速发展,兴趣点(Point-Of-Interest,POI)推荐成为一个重要的研究热点,帮助人们发现有趣的并吸...随着大数据技术的快速发展,推荐系统成为大数据领域里的一个重要的研究方向.随着基于位置社交网络(Location-Based Social Networks,LBSN)的快速发展,兴趣点(Point-Of-Interest,POI)推荐成为一个重要的研究热点,帮助人们发现有趣的并吸引人的位置,特别是当用户在异地旅行的时候.由于用户的签到行为具有高稀疏性,为兴趣点推荐带来很大的挑战.为处理用户签到数据的稀疏性问题,越来越多的研究结合地理影响、时间效应、社会相关性、内容信息和流行度影响这些方面的因素为提高兴趣点推荐的性能.然而,目前的研究缺乏一种综合分析上述所有因素共同作用的方法来处理兴趣点的数据稀疏问题,特别是异地推荐场景被目前大多数研究工作所忽略.针对以上所述的挑战,文中提出一种联合概率生成模型,称为GTSCP,模拟用户签到行为的决策过程,该模型有效地融合上述因素来处理数据稀疏性,特别是异地推荐场景.文章所提的兴趣点推荐方法包含离线模型和在线推荐两个部分.文中所提的GTSCP联合模型支持本地和异地两种推荐场景.文章在多个真实LBSNs的大规模签到数据集上进行实验,结果表明该算法相比其它先进的兴趣点推荐算法具有更好的推荐效果.展开更多
软件缺陷的存在导致软件无法满足用户的需求,如何高效高质量地定位缺陷是消除软件缺陷的关键。基于模型的缺陷定位技术是当前的研究热点,可以用于检测软件系统故障找到软件失效的原因。现有基于模型的缺陷定位技术中,未考虑非相邻节点...软件缺陷的存在导致软件无法满足用户的需求,如何高效高质量地定位缺陷是消除软件缺陷的关键。基于模型的缺陷定位技术是当前的研究热点,可以用于检测软件系统故障找到软件失效的原因。现有基于模型的缺陷定位技术中,未考虑非相邻节点间传递依赖和测试用例对可疑度的影响,导致缺陷定位精度和效率低。提出了基于概率模型检测的软件缺陷定位方法(probabilistic model checking method for software fault location,PMC-SFL),首先提出一种程序概率模型用于提高模型的推理能力;然后设计了基于执行路径构建程序概率模型的学习算法;最后设计了基于概率模型检测的软件缺陷定位算法,用于缺陷定位分析。通过在公共数据集Siemens上进行实验和分析,表明了PMC-SFL方法与五种现有的缺陷定位方法RankCP、BNPDG、Tarantula、SOBER和CT相比,具有更高的软件缺陷定位精度和效率。展开更多
基金supported by the National Natural Science Foundation of China under Grant no. 61371113 and 61401240Graduate Student Research Innovation Program Foundation of Jiangsu Province no. YKC16006+1 种基金Graduate Student Research Innovation Program Foundation of Nantong University no. KYZZ160354Top-notch Academic Programs Project of Jiangsu Higher Education Institutions (PPZY2015B135)
文摘Probabilistic model checking has been widely applied to quantitative analysis of stochastic systems, e.g., analyzing the performance, reliability and survivability of computer and communication systems. In this paper, we extend the application of probabilistic model checking to the vehicle to vehicle(V2V) networks. We first develop a continuous-time Markov chain(CTMC) model for the considered V2V network, after that, the PRISM language is adopted to describe the CTMC model, and continuous-time stochastic logic is used to describe the objective survivability properties. In the analysis, two typical failures are considered, namely the node failure and the link failure, respectively induced by external malicious attacks on a target V2V node, and interrupt in a communication link. Considering these failures, their impacts on the network survivability are demonstrated. It is shown that with increasing failure strength, the network survivability is reduced. On the other hand, the network survivability can be improved with increasing repair rate. The proposed probabilistic model checking-based approach can be effectively used in survivability analysis for the V2V networks, moreover, it is anticipated that the approach can be conveniently extended to other networks.
文摘In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the electricity price at each time. A PBN is widely used as a model of complex systems, and is appropriate as a model of real-time pricing systems. Using the PBN-based model, real-time pricing systems can be quantitatively analyzed. In this paper, we propose a verification method of real-time pricing systems using the PBN-based model and the probabilistic model checker PRISM. First, the PBN-based model is derived. Next, the reachability problem, which is one of the typical verification problems, is formulated, and a solution method is derived. Finally, the effectiveness of the proposed method is presented by a numerical example.
基金supported by the National Natural Science Foundation of China under Grant No.61836005the Australian Research Council under Grant Nos.DP220102059 and DP180100691。
文摘In multiagent systems,agents usually do not have complete information of the whole system,which makes the analysis of such systems hard.The incompleteness of information is normally modelled by means of accessibility relations,and the schedulers consistent with such relations are called uniform.In this paper,we consider probabilistic multiagent systems with accessibility relations and focus on the model checking problem with respect to the probabilistic epistemic temporal logic,which can specify both temporal and epistemic properties.However,the problem is undecidable in general.We show that it becomes decidable when restricted to memoryless uniform schedulers.Then,we present two algorithms for this case:one reduces the model checking problem into a mixed integer non-linear programming(MINLP)problem,which can then be solved by Satisfiability Modulo Theories(SMT)solvers,and the other is an approximate algorithm based on the upper confidence bounds applied to trees(UCT)algorithm,which can return a result whenever queried.These algorithms have been implemented in an existing model checker and then validated on experiments.The experimental results show the efficiency and extendability of these algorithms,and the algorithm based on UCT outperforms the one based on MINLP in most cases.
文摘It is attractive to formulate problems in computer vision and related fields in term of probabilis- tic estimation where the probability models are defined over graphs, such as grammars. The graphical struc- tures, and the state variables defined over them, give a rich knowledge representation which can describe the complex structures of objects and images. The proba- bility distributions defined over the graphs capture the statistical variability of these structures. These proba- bility models can be learnt from training data with lim- ited amounts of supervision. But learning these models suffers from the difficulty of evaluating the normaliza- tion constant, or partition function, of the probability distributions which can be extremely computationally demanding. This paper shows that by placing bounds on the normalization constant we can obtain compu- rationally tractable approximations. Surprisingly, for certain choices of loss functions, we obtain many of the standard max-margin criteria used in support vector machines （SVMs） and hence we reduce the learning to standard machine learning methods. We show that many machine learning methods can be obtained in this way as approximations to probabilistic methods including multi-class max-margin, ordinal regression, max-margin Markov networks and parsers, multiple- instance learning, and latent SVM. We illustrate this work by computer vision applications including image labeling, object detection and localization, and motion estimation. We speculate that rained by using better bounds better results can be ob- and approximations.
文摘随着大数据技术的快速发展,推荐系统成为大数据领域里的一个重要的研究方向.随着基于位置社交网络(Location-Based Social Networks,LBSN)的快速发展,兴趣点(Point-Of-Interest,POI)推荐成为一个重要的研究热点,帮助人们发现有趣的并吸引人的位置,特别是当用户在异地旅行的时候.由于用户的签到行为具有高稀疏性,为兴趣点推荐带来很大的挑战.为处理用户签到数据的稀疏性问题,越来越多的研究结合地理影响、时间效应、社会相关性、内容信息和流行度影响这些方面的因素为提高兴趣点推荐的性能.然而,目前的研究缺乏一种综合分析上述所有因素共同作用的方法来处理兴趣点的数据稀疏问题,特别是异地推荐场景被目前大多数研究工作所忽略.针对以上所述的挑战,文中提出一种联合概率生成模型,称为GTSCP,模拟用户签到行为的决策过程,该模型有效地融合上述因素来处理数据稀疏性,特别是异地推荐场景.文章所提的兴趣点推荐方法包含离线模型和在线推荐两个部分.文中所提的GTSCP联合模型支持本地和异地两种推荐场景.文章在多个真实LBSNs的大规模签到数据集上进行实验,结果表明该算法相比其它先进的兴趣点推荐算法具有更好的推荐效果.
文摘软件缺陷的存在导致软件无法满足用户的需求,如何高效高质量地定位缺陷是消除软件缺陷的关键。基于模型的缺陷定位技术是当前的研究热点,可以用于检测软件系统故障找到软件失效的原因。现有基于模型的缺陷定位技术中,未考虑非相邻节点间传递依赖和测试用例对可疑度的影响,导致缺陷定位精度和效率低。提出了基于概率模型检测的软件缺陷定位方法(probabilistic model checking method for software fault location,PMC-SFL),首先提出一种程序概率模型用于提高模型的推理能力;然后设计了基于执行路径构建程序概率模型的学习算法;最后设计了基于概率模型检测的软件缺陷定位算法,用于缺陷定位分析。通过在公共数据集Siemens上进行实验和分析,表明了PMC-SFL方法与五种现有的缺陷定位方法RankCP、BNPDG、Tarantula、SOBER和CT相比,具有更高的软件缺陷定位精度和效率。
