[moca] Paper announcement: Calcagno, Cardelli, Gordon "Deciding Validity in a Spatial Logic for Trees"

["Andy Gordon" <adg@xxxxxxxxxxxxx>]

We're happy to announce the availability of a new paper.

The paper concerns a spatial logic of trees.  Our logic is a fragment of
various logics of mobile process calculi.  Therefore, we hope our
results are of interest to readers of this list.

Comments are most welcome!

Andy Gordon (on behalf of all three co-authors)

------------------------------------------------------------

Deciding Validity in a Spatial Logic for Trees

Cristiano Calcagno (Queen Mary, University of London)
Luca Cardelli (Microsoft Research)
Andrew D. Gordon (Microsoft Research)

We consider a propositional spatial logic for finite trees.  The logic
includes A|B (spatial composition), and A|>B (the implication induced by
composition), and 0 (the unit of composition). We show that the
satisfaction and validity problems are equivalent, and decidable.  The
crux of the argument is devising a finite enumeration of trees to
consider when deciding whether a spatial implication is satisfied.  We
introduce a sequent calculus for the logic, and show it to be sound and
complete with respect to an interpretation in terms of satisfaction.
Finally, we describe a complete proof procedure for the sequent
calculus.

Available at http://www.luca.demon.co.uk/SpatialLogics.html
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html