On Generalized Records and Spatial Conjunction in Role Logic

paper ps
We have previously introduced role logic as a notation for describing properties of relational structures in shape analysis, databases and knowledge bases. A natural fragment of role logic corresponds to two-variable logic with counting and is therefore decidable. We show how to use role logic to describe open and closed records, as well the dual of records, inverse records. We observe that the spatial conjunction operation of separation logic naturally models record concatenation. Moreover, we show how to eliminate the spatial conjunction of formulas of quantifier depth one in first-order logic with counting. As a result, allowing spatial conjunction of formulas of quantifier depth one preserves the decidability of two-variable logic with counting. This result applies to two-variable role logic fragment as well. The resulting logic smoothly integrates type system and predicate calculus notation and can be viewed as a natural generalization of the notation for constraints arising in role analysis and similar shape analysis approaches.

Citation

Viktor Kuncak and Martin Rinard. On generalized records and spatial conjunction in role logic. Technical Report 942, MIT CSAIL, April 2004. Full version of [32].

BibTex Entry

@techreport{KuncakRinard04OnRecordsSpatialConjunctionRoleLogic,
author = {Viktor Kuncak and Martin Rinard},
title = {On Generalized Records and Spatial Conjunction in Role Logic},
institution = {MIT CSAIL},
number = {942},
year = 2004,
month = {April},
url = {http://arxiv.org/abs/cs.PL/0408019},
note = {Full version of \cite{KuncakRinard04GeneralizedRecordsRoleLogic}},
abstract = {
We have previously introduced role logic as a notation for
describing properties of relational structures in shape
analysis, databases and knowledge bases. A natural fragment
of role logic corresponds to two-variable logic with
counting and is therefore decidable. We show how to use role
logic to describe open and closed records, as well the dual
of records, inverse records. We observe that the spatial
conjunction operation of separation logic naturally models
record concatenation. Moreover, we show how to eliminate the
spatial conjunction of formulas of quantifier depth one in
first-order logic with counting. As a result, allowing
spatial conjunction of formulas of quantifier depth one
preserves the decidability of two-variable logic with
counting. This result applies to two-variable role logic
fragment as well. The resulting logic smoothly integrates
type system and predicate calculus notation and can be
viewed as a natural generalization of the notation for
constraints arising in role analysis and similar shape
analysis approaches.
}
}