Model checking QCTL plus on quantum Markov chains

•The logic QCTL+ extends QCTL by allowing conjunction and negation in atomic path formulas.•A product construction of classical states and the tri-valued truths is presented to tackle conjunctions.•An algebraic approach for the safety of a BSCC spaces is developed under the necessary & sufficient convergence conditions.•A prototype implementation is given in the Wolfram language on Mathematica 11.3.