On the Relationship between Spatial Logics and Behavioral Simulations

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 Schnöbelen, 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 �...

• Type: Conference
• Year: 2010
• Where: FOSSACS
• Authors: Lucia Acciai, Michele Boreale, Gianluigi Zavattaro
• Keywords: Applied Computing, FOSSACS 2010, Petri Nets, Spatial Logic, Transition Systems