Title: Expressing and Verifying Temporal and Structural Properties of Mobile Agents
Authors: Marek A. Bednarczyk, Institute of Computer Science, Polish Academy of Sciences, Gdansk, Poland
   Wojciech Jamroga, Computational Intelligence Group, Clausthal University of Technology
   Wieslaw Pawlowski, Institute of Computer Science, Polish Academy of Sciences, Gdansk, Poland

Abstract:
The paper deals with logics for expressing temporal and structural properties of Petri hypernets, a visual formalism for modeling mobile agents. In particular, we consider how such logics can be built as a composition of two formalisms - one for expressing the temporal, another for expressing the structural properties of multi-agent systems. The problem of model checking properties of a class of composed logics on Petri hypernets is shown to be PSPACE-complete.

Keywords: multi-agent systems, mobile agents, Petri hypernets, temporal logics, model checking.

Computational Intelligence Group @ Technical University of Clausthal Home
Human Media Interaction Group @ University of Twente
Computer Science Group @ University of Gdansk Last modified 2005-11-08