Satisfiability degree computation for linear temporal logic

Temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. The satisfiability degree for temporal logic is introduced in this paper. It is used to precisely express to what extent a model satisfies a property and provides a quantitative analysis of the formal logic model. Then the computation of satisfiability degree for temporal logic is concerned. Based on the discrete-time Markov chains, an intelligent path selection algorithm for the satisfiability degree of the temporal logic is proposed. In the intelligent path selection algorithm the mother states, which are used to form all the paths, is calculated firstly. Those paths satisfy the concerned property and the satisfiability degree expressed by a temporal logic formula is then computed. It is shown that the intelligent path selection algorithm has a polynomial time complexity and O(n2) space complexity. A popular puzzle known as The Ferryman is used to illustrate the feasibility of the intelligent path selection algorithm.