A Mobility Logic for Object Net Systems

Abstract

In this paper we present work in progress on a special variant of Object Petri Nets and on the introduction of a Mobility Logic to reason about them.

The Petri nets considered in this paper allow the vertical transport of net tokens i.e. the transport of net tokens through different nesting levels, giving one enhanced modelling capabilities and allowing one to naturally model certain situations arising in nested structures. The logic then allows us not only to reason about the evolution of the described system in time, but also about spatial configurations, i.e. in this logic we can express for example, that a certain object or agent is always somewhere or at a specific location. This part of our work is inspired by the work of Cardelli and Gordon on the Ambient Calculus and the Ambient Logic.