Semantica temporale debole (WTS)

Informalmente, la semantica temporale debole (Weak Time Semantic, WTS) impone che una transizione possa scattare solo in uno degli istanti identificati dalla sua funzione temporale e non possa scattare prima di essere stata abilitata.

Tuttavia, una transizione non è costretta a scattare anche se abilitata: essa potrebbe scattare, ma non è forzata a farlo. Questo permette di modellare eventi solo parzialmente definiti, ovvero che potrebbero accadere sotto determinate condizioni ma non è possibile dire se lo faranno o no: esempi notevoli sono guasti o decisioni umane, eventi cioè non completamente prevedibili. Si noti che a differenza dei modelli stocastici delle reti di Petri in questo caso non ci interessa la probabilità con cui gli eventi potrebbero accadere, ma solo che potrebbero accadere.

Per imporre questa interpretazione del concetto di tempo l’evoluzione di una rete Time Basic deve seguire i seguenti assiomi temporali:

• (A1) Monotonicità rispetto alla marcatura iniziale: tutti i tempi di scatto di una sequenza di scatto devono essere non minori (\(\geq\)) di uno qualunque dei timestamp dei gettoni della marcatura iniziale.
  Ogni marcatura deve cioè essere consistente, ovvero non contenere gettoni prodotti “nel futuro”.

• (A3) Divergenza del tempo (non-zenonicità): non è possibile avere un numero infinito di scatti in un intervallo di tempo finito.
  Questo assioma serve ad assicurarsi che il tempo avanzi! Esso assicura cioè che il tempo non si possa fermare e soprattutto che esso non possa essere suddivisibile in infinitesimi: il sistema evolve soltanto quando il tempo va avanti.

Le sequenze di scatti che soddisfano questi due assiomi vengono dette sequenze ammissibili in semantica debole.