The Dual Spatial Connectives of Separation Logic

Separation logic has two spatial connectives * and -*. It is known that * and -* are not dual each other, like 'and and 'or', 'for all' and 'there exists', 'necessarily' and 'possibly', etc. To define the dual connectives of * and -* there are two choices: one is to take * and -* as special logical connectives; another is to take * and -* as binary modalities. Correspondingly, the dual modalities of * and -* are represented as the dual connectives of * and *, and as the dual modalities of * and -*, where the latter can be represented by unary modalities in the case that the formulas are defined in a special form.