Hung: 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 con-structs. 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 for-mulas, which express the neighbourhood values of boolean DC state expressions. By establishing a relatively complete axiomatisation for the neighbourhood for-mulas in DC, we then achieve completeness of our system relative to basic DC