@INPROCEEDINGS{ABZ10,
  title = {{On the relationship between spatial logics and behavioral simulations}},
  author = {{Lucia} {Acciai} and {Michele} {Boreale} and {Gianluigi} {Zavattaro}},
  booktitle = {FOSSACS 2010},
  editor = {C.-H. L. Ong},
  abstract = {Spatial logics have been introduced to reason about distributed computation in models for concurrency. We first define a spatial logic for a general class of infinite-state transition systems, the Spatial Transition Systems (sts), where a monoidal structure on states accounts for the spatial dimension. We then show that the model checking problem for this logic is undecidable already when interpreted over Petri nets. Next, building on work by Finkel and Schnobelen, we introduce a subclass of sts, the Well-Structured sts (ws-sts), which is general enough to include such models as Petri nets, Broadcast Protocols, ccs and Weighted Automata. Over ws-sts, an interesting fragment of spatial logic - the monotone fragment - turns out to be decidable under reasonable effectiveness assumptions. For this class of systems, we also offer a Hennessy-Milner theorem, characterizing the logical preorder induced by the monotone fragment as the largest spatial-behavioural simulation. We finally prove that, differently from the corresponding logic, this preorder is in general not decidable, even when confining to effective ws-sts},
  publisher = {Springer Berlin / Heidelberg},
  series = {LNCS},
  volume = {6014},
  year = {2010},
  url = {http://rap.dsi.unifi.it/sensoriasite/ABZ10.pdf},
  keywords = {Behavioural Equivalence, decidability, spatial logic, well-structured (spatial) transition systems},
  partner = {DSIUF, UNIBO},
  status = {public},
  task = {T3.3},
}