Introduction

Behavioral properties may be verified using model checking techniques applied on the reachability graph deduced from petri nets.

Model checking is an automatic technique for verifying finite state concurrent systems. Given the specification of a model and a property, model checking tools answer to the question: Does the model satisfy the property ? An exhaustive search of the state space provides the answer.

This technique suffers from state space explosion problem. With enough memory and time, the procedure terminates. The answer provided is "true" if the model satisfies the property and it is "false" if it does not. In the last case, a counterexample is given.

The model checking tools integrated in CPN-AMI deal with temporal logic properties. On the fly verification and some reduction techniques (symmetric or stubborn set reductions) allow to deal with state space explosion problem.

CPN-AMI integrates three discrete tools for Model Checking:

• GreatSPN and LIP6 tools, a tool comonly developped at the universities of Torino and Genova. Some part of the tool are also developped at LIP6 (reachability graph generation).
  documentation here
  
• PROD, a well known reachability analysis tool for both P/T nets and Coloured nets developed by the Helsinki University of Technology [Varpaaniemi 95]. It is a CTL and LTL model checker;
  documentation here
  
• LoLA, a tool developped at the university Humbolt zu Berlin for the validation of reduction techniques for P/T net reachability graphs. LoLA features symmetric as well as stubborn set based methods. Among LoLA facilities, it is possible to extract information about the reachability graph and toevaluate CTL queries.
  documentation here
  
• Boolcond, a tool developed in our team that computes a boolean condition over P/T net place marking that is respected all over the reachability graph.
  documentation here

The Symbolic reachability graph - GreatSPN and LIP6 tols

Since AMI-Nets are Well Formed Petri Nets, they support the notion of static subclasses that captures a symmetries of a Petri Net specification. This very powerful notion allows to build the symbolic reachability graph and to preserve a lot of space by grouping equivalent "concrete" states (from the Reachability graph) into "symbolic" states (in the reachability graph). We provide here the first tool that exploit the Petri Net structure to automatically compute such classes and get full benefits of the notion.

So, when the Petri net you have designed is syntactically correct, you can reach this menu allows you to do model checking on the symbolic reachability graph (SRG). Symmetries in the system are automatically computed and used by the tool. This allow to work on state spaces that could not be computed using classical techniques.

LTL model checking on the symbolic RG

This service allows to evaluate LTL formulas on the system. Atomic properties are represented by immeidtae transition you may add in the system (you may provide a guard for it). These transitions are fired immediatly when it is possible.

A predefined service allows to check presence of deadlocks in the system.

How to proceed

First of all, it is important to know that atomic properties are observation transitions (that may contain a guard). Our model checker assumes that such a transition has a higher priority and thus, it will tries to fire it at each step of the reachability graph construction. To be identified, these observation transitions must be named with respect to the following convention : transition names must begin with "PROP_". This is the case in the figure below where place PROP_Srest checks if there is at least one idle server in the system.

A small Client server model

To invoke the model checker, please select the "LTL model checking on the symbolic RG" menu. Then a window appears to let you type your formula. For example, the following formula:

G(Srest)

Checks if there is always at least one idles server (this is true the number of client is less than the number of server). The follorwing formula:

GF(Srest)

Checks if eventually a server will become available. A full LYL syntax is provided later in this document.

Understanding Symbolic counter example traces

The answer is either "True" or "False" with a supporting counter-example trace. The trace is a sequence of states that are undesired according to your property, but that your model is capable of.

You can navigate through the sequence using the small arrow-like buttons at the bottom of the result window.

Atomic properties and Formula

The text in the result window gives for each state in the sequence the truth

values of the atomic properties of the formula. t1 means that this property is true, i.e. the current state was reached by firing t1. !t1 indicates that another transition was used to reach this state.

The first line of the result window gives the state of the LTL formula automaton that is synchronized with this state. It describes what part of the formula remains to be satisfied, so it can help to understand what is happening if your formula is complex. This is useful for debugging your formula. It can also be used to follow closely how the synchronized is constructed; if you want to do this, first copy-paste your formula into http://spot.lip6.fr/wiki/TrySpot, negate it by adding a leading '!', and press ok to see the automaton of your negated formula. This is exactly the same automata as used in our engine, so the automaton's state labels correspond to those you see in the counter-example trace.

Symmetries and Permutations

The first item in the result displays a text that gives the equivalence relation that was used in graph construction. It looks something like this :

clients : {c1} {c2,c3,c4}
servers : {s1,s2}
        

You will have one line for each color domain of your model. It explains which elements have been considered equivalent or permutable during graph construction. In this case, client c1 was distinguished from other clients, and both servers were considered equivalent. Essentially this means that in your system, all clients except c1 play the same role.

This is exploited to construct a reduced graph in which, instead of describing a state by saying 'client c2 is idle', we write : 'one of the clients is idle' to represent 'c2 or c3 or c4 is idle' (i.e. the symbolic state represents 3 concrete states here).

Larger sets in the equivalence relation lead to better gains. The worst case is reached when every color domain is fully split as in :

clients : {c1}{c2}{c3}{c4}
servers : {s1}{s2}
        

In that case the symbolic analysis does not offer any reductions of the size of the state space.

You will observe that even if your model is symmetric, your formula may induce asymmetry. Hence some formulae that distinguish specific color domain elements may require construction of a much larger state-space.

Specifying your LTL formula and Atomic properties

You now need to define the property you wish to check on your model.

Using Observation Transitions for Atomic Properties

An observation transition is like a transition of your model, except it is never actually fired. It is used to observe some behavior of your system, hence its name.

The atomic property defined by an observation transition is considered TRUE in any state of the model in which it is enabled.

You may use both pre and inhibitor arcs in your definition of an observation transition, but not post arcs, as it will not be fired anyway. Guards are also allowed on observation transitions.

You may define as many observation transitions as you wish, only those that are used in the LTL formula to be checked will be taken into account at state-space generation time.

For more information on these tools and the principles behind them, the attached attachment:Chap7_theseYTM.pdf is a chapter from Yann Thierry-Mieg thesis (2004) that describes this process. Section 7.3.2 in particular gives example uses of observation transitions.

Defining Observation transitions

An observation transition can be drawn in Macao like a normal transition, just name it PROP_mytransition. The prefix PROP_ will be recognized by the LTL model-checking tools.

If your toto model contains two observing transitions PROP_FOO and PROP_BAR, you can verify the LTL formula FOO U BAR with

("FOO" U BAR)
        

Notes:

• F is an LTL operator, so FOO needs double-quotes (See http://spot.lip6.fr/wiki/LtlSyntax for details.)

LTL is a very expressive subset of the general CTL* temporal logic. See http://en.wikipedia.org/wiki/Specification_patterns_for_finite-state_verification and http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml for examples of linear temporal logic patterns.

The best approach to avoid polluting your model is to define your observation transitions using PetriScript, and keep the script that adds these transitions separate. A minimal PetriScript to add an observation transition would be :

define(PROP_POSX,300)
define(PROP_POSY,300)

-- creation of transitions to check some properties with GreatSPN

create transition "PROP_S3act" (x   PROP_POSX, y PROP_POSY);
connect "<c,3>" place "S_Comp" to transition "PROP_S3act";

create transition "PROP_C1_Send" (x   PROP_POSX, y PROP_POSY); 
connect "<1>" place "Send" to transition "PROP_C1_Send";

create transition "PROP_C1_Rcv" (x   PROP_POSX, y PROP_POSY); 
connect "<1>" place "Rcv" to transition "PROP_C1_Rcv";

The LTL syntax

The table below summarizes the syntax used in the symbolic model checker. Please remind that atomic actions are references to transitions. Please also note that synonyms are available for some LTL commands.

Show symmetric model

This service allows to compute Petri nets static subclasses and the second one display a model that shows these symmetries (for visualization only, the syntax is not supported by CPN-AMI). This is usefull for teaching purpose only.

Display of results

Outputs of GreatSPN are displayed in the historic window. Reachability graphs are downloaded in a new model window (having the appropriate formalism). Let us apply the generation of a symbolic reachability graph on the famous philosopher example (coloured with two philosophers)

Small philosopher example (with two philosophers)

The application of service "Generation of symbolic RG" leads to the construction of a 11 nodes graphs (20 for the reachability graph). The figure below shows a part of this graph (pretty display).

Display of a symbolic reachability graph by GreatSPN2 in CPN-AMI.

Let us consider a marking (expanded in the Figure below) from the symbolic reachability graph of the philosopher model. The symbolic marking indicates that:

• the place thinking is marked by one philosopher (<static_C1> with cardinality equal to 1),
• The place wait_left is marked by one philosopher (<static_C0> with cardinality equal to 1),
• The place ok_right is marked by one philosopher (<static_C0> with cardinality equal to 1),
• The place forks is marked by one philosopher (<static_C0> with cardinality equal to 1).

Known Problems:

1. in this version, there is still a problem (being corrected) in GreatSPN with the predecessor function. This function whould not take place in arc valuations;
2. this version is not yet available on solaris.

Model checking with PROD

PROD has been integrated in CPN-AMI 2. Therefore it is possible to construct nets graphically and to use PROD functionalities without leaving the CPN-AMI environment. PROD is a rich but complex tool. So, we have encapsulated a set of usefull queries. Of course, the user can directly enter PROD queries for more precise and complex evaluation of a Petri net.

The PROD service menu

The structuyre of PROD service is shown below. Services are outline in red.

When the Petri net you have designed is syntactically correct, you can reach the PROD menu on which two services are reachable: "PROD on the fly" and "Construction of the reachability Graph":

• The first service produces a program that is dedicated to on the fly verification of a LTL query (you introduce by means of a dialog window). On the fly verification means that the formula is checked during the graph construction.
• The second one generates the reachability graph for the model you opened. To reach other services, you must run this one first. You then get the following Menu.

The Graph construction (on the fly or not) may take a very long time (especially when the reachability graph is not finite;-). So, you can cancel it by clicking on the STOP button in the execution window. If you do so, you will have to run "Set the reachability Graph (interrupted construction)" before running other services. In this case, queries only concern the computed nodes. The verification results may be computed again each time new nodes are computed.

When a (sub)graph has been produced, you can run the following queries:

• Generate the Reachability Graph (to get a new one or to continue the graph if it is not yet finished);
• Display statistics about the reachability graph (number of generated nodes, number of arcs, number of terminal nodes...);
• List dead markings;
• Get a path between two nodes (referenced by their PROD identifier:
  • For long path, the non verbose mode provides a minimal information,
  • Verbose mode provides full information as PROD does,
  • Animation provides a more friendly animation by means of the Macao result window system enabling to view on the model elements to be affected by the net evolution.
• Test if a place can be emptied in a reachable state . Please note that you must select the place before running this service;
• Get the list of Reachability graph's states for which a given place is empty. Please note that you must select the place before running this service;
• Display the reachability graph. This service is usefull for small reachability graphs. A layout is computed for nodes (it takes a long time for large graphs but it is pretty). You may also compute a route for arcs (even prettier but also slower);
• Evaluate a CTL query in expert mode. Some basic syntactic elements of the CTL available in PROD is provided here.
• Clean PROD files, which is usefull to save space on the server's hard disk.

Several options are available to generate the reachability graph.:

• "New graph" allows you to generate a new graph from the begining. It can be used if you want to delete the previous graph;
• "Bound execution time" allows you to specify the maximum time you want to wait (in minutes). The execution will automatically stop when this limit is reached;
• "Bound number of nodes" allows you to specify the maximum number of nodes you want to generate. The execution will automatically stop when this limit is reached,
• "Use Memory" (checked by default) automatically allocate 16Mb of RAM to the PROD graph generator in order to speed up the Graph generation.

Display of results

Most results are displayed on the historic window, except for the reachability graph that is generated in a new model window (using the formalism ReachabilityGraph). We will focuse on the execution of this service.

A small example model.

Let us imagine that we have generated the full reachability graph for this model and that we find it is of interest to display it. By invoking the service " Display the reachability graph - arc routing", we get the following informations in the historic window.

Information provided by PROD in CPN-AMI during its execution.

We also get the following graph.

The produced reachability graph.

Please note that, to increase readability of the graph, terminal nodes are black and the initial node is double bordered. Let us decode the state description of the first deadlock we detect (black node at the left). It says : "D: 2<..>" which means that place B contains two non colored tokens. When a token is colored, its value is expressed between "<." and ".>".

CTL or LTL queries with PROD

The LTL prod "on the fly" mode allows you to process LTL queries during the reachability Graph construction. The Expert mode has been introduced to enable the definition of CTL queries. In the current version of PROD in CPN-AMI, you can use either PROD syntax or CTL syntax to express your CTL queries. First, select the appropriate menu to launch your query.

Then a window appear. Just type your query and click on OK to process it. We assume this query is being sent to the model example provided to illustrate the Reachability Graph generation.

Example of CTL Query on the example model.

The result appears on the historic window and you are back to a new dialog box to strike a new query (the last query is maintained to ease correction of errors). When you have finished with the expert mode click on "Cancel" to exit.

The historic window and the result of a PROD query.

List of CTL commands for the Expert mode

Herafter is the syntax of CTL formulas. For more details, please have a look on the PROD user manual.

Warning: PROD LTL formulas syntax is not the same, please refer to the prod documentation to get information on this syntax.

Access to PROD documentation

You can get the PROD documentation (main document and errata) as pdf documents or go to the PROD web site to get it (compressed PS files).

Symbolic reachability graph - GreatSPN and liP6 tools

A Symbolic Reachability Graph (SRG) is a highly condensed representation of the reachability graph built automatically from a specification of system in terms of Well-formed net. The building of such graph profits from the presence of object symmetries to aggregate either states or actions within symbolic representatives (equivalence classes).The equivalence relation between states is based on structural symmetries which are directly read off from the types of objects defined in the system specification. By definingconvenient types of actions for these types of objects, it can be ensured that states which are equivalent let the future behavior of the system unchanged. SRG gathers the following advantages: to be built automatically from the Well-formed net specification, and, to enable efficient symbolic approach by defining canonical symbolic representatives of states and actions.

Model Checking with LoLA (not yet available on mac)

LoLA (a Low Level Petri Net Analyzer) has been implemented for the validation of reduction techniques for place/transition net reachability graphs. LoLA features symmetric as well as stubborn set based methods. Net symmetries are automatically computed. Stubborn sets are customized to the particular analysis task. LoLA can analyze reachability of a given state or state predicate, boundedness of the net or a place, deadlocks, dead transitions, reversibility, and existence of home states. LoLA can verify formulas of a branching time logic. Additionally, there is a memory-efficient semi-decision procedure for the satisfiability of a given state predicate.

Model Checking functions of LoLA can compute:

• Reachability of a given state or state predicate
• Quasiliveness of a given transition
• Reversibility of the net
• Existence of home states
• Model checking for a branching time temporal logic
• 1 memoryless search for a path to a given state predicate

All problems are verified by exploring the state space. The following reduction techniques have been integrated when possibleavailable:

• Symmetric reduction
• Stubborn set reduction
• Coverability graph reduction

For more information on LoLA, please check with the documentation on the official web site.

Thanks to Karsten Schmidt for his contribution and the efficiency of his tool.

The LoLA service menu

When a P/T net has been succesfuly syntacticaly checked, you can reach the LoLA menus in the model checking section (services are in red). Please note that the service "is a transition dead" requires a transition to be selected.

Display of Results (service with no formula)

Let us consider the model below on wich we check the presence of a home state using the corresponding service in LoLA.

Small P/T net to be analyzed.

The result of this service is presented below. Please note that, when a LoLAservice is invoked for the first time, a compilation is performed to customize an executable. This is due to the LoLA behavior. The only incidence is that the first execution of a LoLA service is a little longer than other ones.

Result of service "is there a home stae?"

Display of Results (service requiring a formula)

Some services require either a state predicate formula or a CTL formula. Then, a text window appear to let the user type this formula. More information on the LoLA languages is provided here. You may also have a look on the full documentation. Please note that we only consider P/T net for the moment.

As claimed in the LoLA user manual, a predicate formula has the same syntax than a CTL formula but some operators are prohibed: ALLPATH, EXPATH, EVENTUALLY, ALWAYS, UNTIL and NEXTSTEP must not appear.

The formula below checks that place AMC has more than two tokens.

The formula to be processed

The result of this formula is displayed in the historic window. In our case, it is false.

Result from the query evaluation.

Computation of behavioral bounds

Let us consider the following model on wich we want to test if place P5 is bounded.

Model to check

The display is shown below. Please note that, when a LoLAservice is invoked for the first time, a compilation is performed to customize an executable. This is due to the LoLA behavior. The only incidence is that the first execution of a LoLA service is a little longer than other ones.

Result from a LoLA based service.

Computation of Logic Formulae over Place Marking

The marked trap property (resp. unmarked deadlocks) means that, for any reachable state, a set of places contains at least a token (resp. contains no token). These properties can be written using logical formulæ, for which variables express that a place contains, or not, at least one token. Of course, those formulæ have a special frame.

The tool we present computes properties for a Place/Transition Petri net with inhibitor arcs [Paviot 95]. The properties are written in the same kind of logical formulæ, but with a general shape. They, thus, express more general properties than traps and deadlocks do. This tool does not ensure that a generative family is computed, however, more information are generaly computed than the one obtained using only Traps and Deadloocks. Further information can be automatically obtained using Flows and SemiFlows.

The service Menu

When the P/T net you have designed is syntactically correct, you can reach the corresponding menu item (in red). By selecting this service, you launch the application.

Display of results

Results are displayed in Macao historic window. We provide here two examples having discrete characteristics. This model has three places in wich one token moves.

First Petri net example (safe or 1-bounded).

The service provides the following information (see below). The model is safe (1-bounded) and any reachable marking respects the following logic fomulae:

P3 is marked or P2 is marked or P1 is marked and
P2 is not marked or P1 is not marked and
P3 is not marked or P1 is not marked and
P3 is not marked or P2 is not marked

Result of the BooleanCondition service.

If the model is not safe (1-bounded), unsafe places are outlined and the computed result is usually less interesting. Let us consider the following model which is not safe (two tokens are runnning over the set of places).

Second Petri net example (not safe).

As you can see below, the tool mentions unsafe places and provides a smaller result. The condition for any marking is now:

P1 is marked or P2 is marked or P3 is marked