A complete fragment of higher-order duration μ-calculus

Abstract

The paper presents an extension μHDC of Higher-order Duration Calculus (HDC,[ZGZ99]) by a polyadic least fixed point (μ) operator and a class of non-logical symbols with a finite variability restriction on their interpretations, which classifies these symbols as intermediate between rigid symbols and flexible symbols as known in DC. The μ operator and the new kind of symbols enable straightforward specification of recursion and data manipulation by HDC. The paper contains a completeness theorem about an extension of the proof system for HDC by axioms about μ and symbols of finite variability for a class of simple μHDC formulas. The completeness theorem is proved by the method of local elimination of the extending operator μ, which was earlier used for a similar purpose in [Gue98].