A Complete Fragment of Higher-Order Duration $\mu$-Calculus

Dimitar P. Guelev

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


Abstract

The paper presents an extension of Higher-order Duration Calculus (HDC,Zhou, Guelev and Zhan, 1999) 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 least fixed point 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 the new operator and symbols of finite variability for a class of so called simple formulas, which extends the original class of simple formulas in DC with iteration introduced in (Dang and Wang, 1994). The new class extends the original one by allowing subformulas of finite variability and existential quantification over both individual and program variables. The completeness theorem is proved by the method of local elimination of the extending operator, which was earlier used for a similar purpose in (Guelev, 1998). Simple formulas suffice to accommodate specification of Verilog semantics by HDC as in (Zhu and He, 2000). The axioms about polyadic least fixed point operator are paraphrases of the rules known from the propositional modal mu-calculus(Kozen, 1983).


Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Maintainer fsttcs20@cse.iitd.ernet.in.
Start Conference Manager
Conference Systems