On The Quantitative And Optimized Algorithms For Deciding The Monitorability Of Linear Temporal Logic Formulas

The decision of monitorability and weak monitorability are often used to measure whether a given linear temporal logic formula is suitable for runtime verification.There are mainly three kinds of decision algorithms for monitorability and weak monitorability: a Monitor-based decision algorithm,a Formula-rewriting-based decision algorithm and an Infinite-obligation-formulas-based decision algorithm.Among them,the last decision algorithm is an incomplete algorithm,which can only be used simultaneously with the other two algorithms to speed up the decision of them.However,the existing research on monitorability and weak monitorability has two defects.First,in practical runtime verification,the definition of monitorability is too strict,which requires that all finite traces are monitorable,and the definition of weak monitorability is too loose,which only requires that one monitorable finite trace exists.Therefore,we cannot accurately quantify the value of a formula in runtime verification.Second,for the decision algorithm of weak monitorability,the Formularewriting-based decision algorithm should theoretically be superior to the Monitor-based decision algorithm,but we get the opposite conclusion in most experiments,that is,the Monitor-based decision algorithm is superior to the Formula-rewriting-based decision algorithm.The main reason is that the existing Formula-rewriting-based decision algorithm lacks effective optimization technology.In this paper,we propose new solutions to the above two issues.First,we propose the definition of probabilistic monitorability to quantify the value of a linear temporal logic formula in runtime verification,and introduce a Definition-based solution algorithm and a Monitor-based solution algorithm.Then,we implement the Monitor-based solution algorithm using probabilistic model checker PRISM and SMT solvers Z3 and CVC4.Second,for the Formula-rewriting-based decision algorithm of weak monitorability,we propose four-point optimization for it: Dynamically obtain the successor formulas.Determine the existence of the eternal truth and contradiction in the successor formulas in advance.SAT solver tries to determine the simpler formula in the same ring as much as possible.The infinite obligation formula speeds up the four-value solution of weak monitorability.Last,we design and implement a prototype system tool—monic to verify the correctness and efficiency of the algorithm proposed in this paper,which combines probabilistic monitorability solution and weak monitorability decision.Experimental results show that our algorithms are correct,and the SMT-solver-based implementation is significantly more efficient than the PRISM-based implementation.In addition,compared with the algorithm before optimization,the optimized Formularewriting-based decision algorithm has an average improvement of 53.6% in decision efficiency,and it is better than the Monitor-based decision algorithm in 81.0%.