Sciweavers

Share
FOSSACS
2010
Springer

On the Relationship between Spatial Logics and Behavioral Simulations

9 years 10 months ago
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 ...
Lucia Acciai, Michele Boreale, Gianluigi Zavattaro
Added 28 May 2010
Updated 28 May 2010
Type Conference
Year 2010
Where FOSSACS
Authors Lucia Acciai, Michele Boreale, Gianluigi Zavattaro
Comments (0)
books