×

Recursive mean-value calculus. (English) Zbl 0928.03020

Arvind, V. (ed.) et al., Foundations of software technology and theoretical computer science. 18th conference, Chennai, India, December 17–19, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1530, 257-268 (1998).
Summary: The Mean-Value Calculus, MVC, of C. Zhou and X. Li [“A mean value calculus of durations”, in: A. W. Roscoe (ed.), A classical mind: Essays in honour of C. A. R. Hoare (Prentice Hall), 431-451 (1994)] is extended with the least and greatest fixed point operators. The resulting logic is called \(\mu\text{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 \(\mu\text{MVC}\) over both dense and discrete times is undecidable.
For the entire collection see [Zbl 0903.00078].

MSC:

03B44 Temporal logic
03B70 Logic in computer science
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite