Expressing and Verifying Temporal and Structural Properties of Mobile Agents

Issue title: SPECIAL ISSUE ON CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P 2005) Ruciane-Nide, Poland, 28–30 September 2005

Article type: Research Article

Authors: Bednarczyk, Marek A. | Jamroga, Wojciech | Pawłowski, Wiesław

Affiliations: Institute of Computer Science, Polish Academy of Sciences, Gdańsk, Poland. E-mail: [email protected] | Chair of Computational Intelligence, Clausthal University of Technology, Germany. E-mail: [email protected]

Abstract: 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 problemof model checking properties of a class of the logic on Petri hypernets is shown to be PSPACE-complete.

Keywords: dynamic mobile agents, dynamic mobile agents, temporal logics, model checking

Journal: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 51-63, 2006