Recursive Mean-Value Calculus

The Mean-Value Calculus, MVC, of Zhou and Li [19] is extended with the least and the greatest fixed point operators. The resulting logic is called μMVC. Timed behaviours with naturally recursive structure can be elegantly specified in this logic. Some examples of such usage are given. The expressive power of the logic is also studied. It is shown that the propositional fragment of the logic, even with discrete time, is powerful enough to encode the computations of nondeterministic turing machines. Hence, the satisfiability of propositional μMVC over both dense and discrete times is undecidedable.