Prefix and Projection onto State in Duration Calculus

Abstract

We study a new operator of projection onto state and the prefix operator in the extension μHDC of DC by quantifiers over state and a polyadic least fixed point operator. We give axioms and rules to enable deduction in the extension of μHDC by the new operators. Our axioms can be used to eliminate the new operators from formulas in a practically significant fragment of μHDC. This entails the decidability of certain subfragments of this fragment is preserved in the presence of the new operators.