Prefix and Projection onto State in Duration Calculus
この論文をさがす
説明
AbstractWe 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.
収録刊行物
-
- Electronic Notes in Theoretical Computer Science
-
Electronic Notes in Theoretical Computer Science 65 101-119, 2002-06-01
Elsevier BV