Temporal logic for state spaces

Temporal logic for state spaces

These facilities make it possible to analyze state spaces by means of a CTL-like temporal logic. It is possible to formulate queries about states, but also queries about state changes (e.g., the occurrence of certain transitions). Strongly connected components are used to make the model checking more efficient. ┬áManual A manual describing how to use the temporal logic facilities is available. Note that even though […]

Read Me Leave comment

States and state space nodes

States and state space nodes

The state of a CPN is a marking of the net, i.e. a distribution of tokens on the places of the net. Each node in a state space represents a state/marking of the corresponding CPN. It is possible to transfer states between the simulator and the state space tool. Nodes, i.e. states, in a state space are denoted by positive integers. By convention, 1 denotes […]

Read Me Leave comment