Formal analysis of information flow and control properties in Petri nets

In this work we study formal techniques for studying information flow and control properties in distributed systems modelled with Petri nets. The first problem that we tackle consists in checking whether an agent observing only part of a system is able to gather information about the hidden part. We study this problem starting from two formal relations defined in the literature on the transitions of the Petri net: reveals and excludes. Reveals models positive information flow, meaning that the observation of a transition gives information about the occurrence of another one; \emph{excludes} models negative information flow, meaning that observing a transition gives information about the non-occurrence of another one. We define some generalizations of these two relations and propose several algorithms to compute them on a particular class of Petri nets. We then consider a control problem: we assume that an agent can control only some transitions on the Petri net and observe only some places; we want to know whether the agent is able to enforce certain properties on the system. We model the problem as a two-player asynchronous game on the Petri net and study notions of observation that keep into account the concurrent nature of the system. We propose algorithms to find strategies in some particular cases, making use both of the unfolding and of the marking graph, and we study the relation between our model and concurrent game structures, introduced to define the game-based temporal logic ATL. Finally, we start to explore the use of Petri nets to model asynchronous multi-agent system. We consider a model defined on automata and show that it can be equivalently expressed with Petri nets, possibly in a more compact way.

In questa tesi studiamo tecniche formali per l'analisi del flusso di informazioni e per verificare proprietà di controllo in sistemi distribuiti modellati con reti di Petri. Il problema che affrontiamo consiste nel verificare se un agente che osserva solo una parte di un sistema è in grado di ottenere informazioni sulla parte nascosta. Studiamo questo problema partendo da due relazioni formali definite nella letteratura sulle transizioni della rete di Petri: reveals e excludes. Reveals modella un flusso di informazione positivo, ossia modella il fatto che dall'osservazione di una transizione della rete di Petri si deduce l'occorrenza di una transizione non osservabile; excludes modella un flusso di informazione negativo, ossia modella il fatto che dall'osservazione di una transizione della rete si deduce che un'altra non può essere occorsa. Consideriamo poi un problema di controllo: assumiamo che un agente possa controllare solo una parte delle transizioni della rete e osservare solo alcuni posti; vogliamo sapere se l'agente è in grado di forzare alcune proprietà sul sistema. Modelliamo il problema come un gioco asincrono a due giocatori sulla rete di Petri e studiamo nozioni di osservazione che tengano conto della natura concorrente del sistema. Proponiamo algoritmi per trovare strategie in alcuni casi particolari, facendo uso sia dell'unfolding che del grafo delle marcature, e studiamo la relazione tra il nostro modello e il modello delle strutture gioco concorrenti, introdotte per definire la logica temporale basata sui giochi ATL. Infine, esploriamo l'uso delle reti di Petri per modellare sistemi multi-agente asincroni. Consideriamo un modello definito sugli automi e mostriamo che può essere equivalentemente espresso attraverso le reti di Petri, in alcuni casi in modo più compatto rispetto alla rappresentazione con gli automi.