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.


A manual describing how to use the temporal logic facilities is available. Note that even though the manual is written for use with another tool, much of it is applicable to CPN Tools.

The manual describes how to install and load the facilities. These descriptions do not apply to CPN Tools. In version 1.2 (and after) of CPN Tools, it is no longer necessary to install the facilities, and the steps for loading the facilities are described below.

Loading the facilities

Before the temporal logic facilities can be used, some additional information must be loaded into the state space tool. To load the facilities you must:


The ML code can be created with the Create auxiliary text tool and evaluated with the Evaluate ML tool.

Example net

This net can be found in a subdir of cpntools called Samples\\DiningPhilosophers.

Additional information

Additional information about the facilities is available online:

Related pages