A Relatively Complete Axiomatisation of Projection Onto State in the Duration Calculus

We present a complete axiomatisation of the operator of projection onto state in the Duration Calculus (DC) relative to validity in DC without extending constructs. Projection onto state was introduced and studied extensively in our earlier works. We first establish the completeness of a system of axioms and proof rules for the operator relative to validity in the extension of DC by neighbourhood formulas, which express the neighbourhood values of boolean DC state expressions. By establishing a relatively complete axiomatisation for the neighbourhood formulas in DC, we then achieve completeness of our system relative to basic DC.