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.

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:

• Enter the state space tool
• Calculating the state space (including the SCC graph)
• Evaluate the following ML code: use (ogpath^”/ASKCTL/ASKCTLloader.sml”)

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

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

Additional information about the facilities is available online:

• Technical report
• Slide presentation

Verification