Expressing and Verifying Temporal and Structural Properties of Mobile Agents

Logics for expressing properties of Petri hypernets, a visual formalism for modelling mobile agents, are proposed. Two classes of properties are of interest--the temporal evolution of agents and their structural correlation. In particular, we investigate how the classes can be combined into a logic capable of expressing the dynamic evolution of the structural correlation. The problem of model checking properties of a class of the logic on Petri hypernets is shown to be PSPACE-complete.

• Type: Journal
• Year: 2006
• Where: FUIN
• Authors: Marek A. Bednarczyk, Wojciech Jamroga, Wieslaw Pawlowski
• Keywords: FUIN 2006, Logic, Petri Hypernets, Structural Correlation