Mu-calculus (a.k.a. $\mu$TL) is built up from modal/dynamic logic via adding the least fixpoint operator $\mu$. This type of logic has attracted increasing attention since Kozen’s seminal work. P $\mu$TL is a succinct probabilistic extension of the standard $\mu$TL obtained by making the modal operators probabilistic. Properties of this logic, such as expressiveness and satisfiability decision, have been studied elsewhere. We consider another important problem: the axiomatization of that logic. By extending the approaches of Kozen and Walukiewicz, we present an axiom system for P $\mu$TL. In addition, we show that the axiom system is complete for aconjunctive formulas.

Neural networks, as an important computing model, have a wide application in artificial intelligence (AI) domain. From the perspective of computer science, such a computing model requires a formal description of its behaviors, particularly the relation between input and output. In addition, such specifications ought to be verified automatically. ReLU (rectified linear unit) neural networks are intensively used in practice. In this paper, we present ReLU Temporal Logic (ReTL), whose semantics is defined with respect to ReLU neural networks, which could specify value-related properties about the network. We show that the model checking algorithm for the Σ₂ ∪ Π₂ fragment of ReTL, which can express properties such as output reachability, is decidable in EXPSPACE. We have also implemented our algorithm with a prototype tool, and experimental results demonstrate the feasibility of the presented model checking approach.