Symbolic Soundness Verification of Data Petri Net

Data Petri Nets are still a niche topic and this is demonstrated by the little documentation that is available online. However, they may have important applications especially within concurrent and discrete-event systems. However, a generated DPN must respect the Soundness properties, i.e. those properties that guarantee the proper functioning of the system. In a system a series of events can occur in a certain order and to be correct we must be sure that no possible combination of events can lead to inconsistent results. In order to work with Data Petri Nets, it is essential to have a better understanding of how standard Petri Nets work, and therefore without data. Only then is it possible to study its extension with data and by importing the concepts of constraint programming. While in basic petri nets the transitions are limited to consuming tokens from the incoming place and adding them to the outgoing place, in the DPN a constraint will be represented in the transition and the task of our program is to verify whether this constraint will always be respected, will never be respected or whether in some cases it will be respected and in others not. In logic programming, constraints can be of many types, but in this program we will only deal with logical constraints that use one of the six relational operators (=,̸=,>,<, ≥, ≤) which will relate a variable to a constant, or a variable to another variable. The domain of these variables is represented by the set of real numbers R , however in the program it was decided to also manage boolean variables and which therefore can assume true or false values. After defining the field of application it is essential to find a way to verify the correctness of the system and to do this we proceed as is normally done for logic programming problems: with the construction of the Constraint Graph. Through the im- plementation of the algorithms that are detailed in the drafting of this thesis it is possible to verify the correctness of a DPN, knowing that DPN and Constraint Graph are related to each other through the obs-simulation, so if the Constraint Graph is data-aware sound, then the DPN is also data-aware sound.

Le Data Petri Net sono ancora un argomento di nicchia e questo è dimostrato dalla poca documen- tazione che si trova online. Tuttavia possono avere applicazioni importanti soprattutto nell’ambito dei sistemi concorrenti e a eventi discreti. Tuttavia un DPN generato deve rispettare le proprietà di Soundness, ovvero quelle proprietà che garantiscono il buon funzionamento del sistema. In un sistema possono verificarsi una serie di eventi in un certo ordine e per essere corretto dobbiamo essere sicuri che nessuna possibile combinazione di eventi possa portare a risultati inconsistenti. Per poter lavorare con le Data Petri Net è fondamentale aver compreso al meglio il funzionamento delle Petri Net standard e quindi senza dati. Solo dopo è possibile studiare la sua estensione con dati e importando i concetti della programmazione a vincoli. Mentre nelle reti di petri di base le transizioni si limitano a consumare token dal place entrante e aggiungerne al place uscente, nelle DPN nella transizione sarà rappresentato un vincolo e compito del nostro programma è verificare se questo vincolo sarà sempre rispettato, non sarà mai rispettato oppure se in alcuni casi sarà rispettato e in altri no. Nella programmazione logica i vincoli possono essere di molti tipi, ma in questo programma ci si occuperà solamente di vincoli logici che usano uno dei sei operatori relazionali (=,̸=,>,<, ≥, ≤) che metteranno in relazione una variabile con una costante, oppure una variabile con un’altra variabile. Il dominio di queste variabili è rappresentato dall’insieme dei numeri reali R , tuttavia nel programma si è deciso di gestire anche variabili booleane e che quindi possono assumere valori true o false. Dopo aver definito il campo di applicazione è fondamentale trovare un modo per verificare la correttezza del sistema e per fare questo si provvede come di norma viene fatto per i problemi di programmazione logica: con la costruzione del Constraint Graph. Attraverso l’implementazione degli algoritmi che vengono approfonditi nella stesura di questa tesi è possibile verificare la correttezza di un DPN, sapendo che DPN e Constraint Graph sono in relazione tra loro attraverso la obs-simulation, per cui se il Constraint Graph è data-aware sound, allora anche il DPN è data-aware sound.