Cos'è lo stato e da dove viene, quando si genera grafici di raggiungibilità

Question

Per Automata a tempo, Ho trovato Figura 1 sotto. Per Reti di Petri colorate ho trovato figura 2. Entrambi sono per "Grafico di raggiungibilità Costruzione".

Tuttavia, non descrivono dove hanno ottenuto il stati da (Figura 3), per generare il grafico di raggiungibilità. Presumono che tu abbia "stati" per generare un grafico di raggiungibilità, ma non sono sicuro di cosa siano questi stati. Nel caso Automata a tempo, non sono sicuro che gli "stati" di automi siano ciò che stanno descrivendo, sembra che per "stato" significano il Stato del programma Dopo l'esecuzione degli automi (o su ogni passaggio). Allo stesso modo per le reti di Petri, lo stato non è il luogo o la transizione, ma lo stato del programma. Almeno questo è quello che sto ottenendo.

Detto questo, la mia domanda è Come costruire lo stato del programma, in modo che io possa quindi costruire il grafico di raggiungibilità. Inoltre, mi chiedo di cosa siano effettivamente composti gli stati. Cosa lo stato è (predicati booleani, espressioni logiche temporali, dati, ecc.).

Qualche dettaglio in più. Da qui (sulle reti di Petri):

Un marcatura $ m '$ è raggiungibile da un marchio $ m $ se $ m [s rangle m' $ per alcuni $ s in t^*$ ... il set di raggiungimento della portabilità (n) di n è l'insieme di Tutti i segni che sono raggiungibili dalla marcatura iniziale. [I segni hanno a che fare con i dati associati a un luogo (un nodo netto di Petri)] ... una rete di Petri $ n = (p, t, f, m_0) $ induce diverse strutture standard su cui le logiche del primo ordine possono essere interpretato ... per specificare le proprietà delle strutture ... ottenute da una rete di Petri $ n $, introduciamo una logica del primo ordine FO con predicati atomici da $ x a y $, $ x overset {*} { a } y $, $ x overset {+} { a} y $ e $ init (x) $. [Quindi entrano nella parte di controllo del modello].

Ciò dimostra solo come la costruzione del grafico di raggiungibilità viene esclusa. Cioè, ciò che è composto (in dettaglio) e come costruirlo.

---

Figura 1 $ Downarrow $

Figura 2 $ downarrow $

Figura 3 $ downarrow $