We propose a simple but effective method for the detection of duplicates in state predicates for Petri nets. We map sub-formulas to integer numbers using a mapping abstr. The assignment guarantees that abstr( 1) = abstr( 2) implies equivalence of 1 and 2 while abstr( 1) = abstr( 2) implies equivalence of 1 and : 2. The obtained knowledge can be used for reducing the size of a formula that is obtained by expensive constructions such as the transformation into disjunctive normal form. The method is implemented in our tool LoLA 2.0.
We consider place/transition nets. A place/transition net N consists of finite and disjoint sets P (places) and T (transitions), an arc relation F (P T )[(T P ), a weight function W : F ! N n f0g, and an initial marking m0. A marking m is a mapping m : P ! N. Transition t is enabled in m iff, for all p 2 P , [p; t] 2 F implies m(p) W ([p; t]).
We skip the definition of the behaviour of Petri nets since this is not relevant for this paper. 3
A state predicate is a logical formula that represents a property of markings. Applied to a marking, it yields true or false. State predicates are used for the specification of verification queries, typically as part of a formula in some temporal logic. Most verification tools for Petri nets support the specification of state predicates in one or the other syntax. Most competitions in the model checking contest (MCC) [3] involve state predicates. Our considerations are based on the following syntax and semantics.
Definition 1 (State predicate). A state predicate can have any of the following shapes (ki are integer numbers, pi are places, ti transitions, 2 f<; >; ; ; =; 6=g, and i state predicates): – TRUE, FALSE: true for all markings (no marking, respectively); – k1p1 + + knpn k0: true for marking m iff k1m(p1) + + knm(pn) – FIREABLE(ti): true for m iff ti is enabled in m; – DEADLOCK: true for m iff no transition is enabled in m; – INITIAL: true for m iff m = m0; –
1 ^ ^ n, 1 _ _ n, : 1, 1 =) 2, 1 () to the usual interpretation of Boolean logic. 2: evaluated according k0;
State predicates can be represented as a tree, with the Boolean operators as inner nodes and the remaining predicates (called atomic) as leaves. We assume that a conjunction 1 ^ ^ n is represented as a single node with n children for the sub-formulas i. The same applies to disjunctions. 4
There are several transformations that involve replication of subformulas:
Rewriting Boolean operators. Even if all Boolean operators are permitted in specifications, internal representations are usually restricted to conjunction and disjunction. That is, 1 () 2 may be replaced with ( 1 ^ 2) _ (: 1 ^ : 2) and causes a replication of sub-formulas 1 and 2. Similar rewriting rules apply to formulas in temporal logic, causing replication of involved state predicates.
Rewriting atomic predicates. Tools typically try to internally use as few as possible atomic state predicates. So FIREABLE(t) can be replaced by Vp:[p;t]2F p
W ([p; t]). INITIAL can be replaced with Vp2P p = m0(p). DEADLOCK is equivalent to Vt2T : FIREABLE(t). The overwhelming majority of Petri net models is ordinary (all arc weights are equal to one) and a considerable amount of models is safe (at most one token on any place in all reachable markings). For example, the “known models” of the MCC in 2017 comprised of 65 ordinary nets versus 12 non-ordinary nets. 39 nets are safe, compared to 38 non-safe net models.
predicates like p > 0 and p = 1 may occur several times (e.g. once for every transition connected to p).
Frequently used predicates. Many specifications frequently use expressions like “place p is marked (p > 0)” or “ p is unmarked (p = 0)”. Hence, these predicates may occur more than once in a predicate.
Transformation into disjunctive normal form. Verification techniques that are based on linear algebra, for instance the exploitation of the state equation [6], are restricted to convex properties (i.e. conjunctions of inequations). Hence, FIREABILITY and other predicates must be unfolded and the resulting property must be transformed into a disjunction of conjunctions of inequations. Then, the individual conjunctions can be fed to the state equation separately. Generation of a disjunctive normal form involves the application of the law of distributivity: ( 1 _ 2 _ 3) ^ ( 4 _ 5) is to be rewritten to ( 1 ^ 4) _ ( 1 ^ 5) _ ( 2 ^ 4) _ ( 2 ^ 5) _ ( 3 ^ 4) _ ( 3 ^ 5).
Translation from other formalisms. Place/transition nets representing interesting systems, together with their verification queries, are often generated by translation from other specification languages. Translations are based on patterns and often induce duplicates of state predicates or sub-formulas. Consider, for instance, the translation from a place p of a Coloured Petri Net with domain f1; 2; 3g into three places p1, p2, and p3 of a place/transition net. Assuming that addition is not supported, formula p = (three tokens on p) could be translated into (p1 = 0^p2 = 0^p3 = 3)_(p1 = 0^p2 = 1^p3 = 2)_ _(p1 = 3^p2 = 0^p3 = 0) This formula contains a lot of replications of elementary comparisons.
Consequently, a verification tool may expect the presence of duplicates in the state predicates it is given for verification. It generates additional duplicates in its internal transformations. Since place/transition nets are a formalism with low-level modelling primitives (transitions actually represent simple vector addition), automatically generated predicates may involve huge conjunctions and disjunctions. Generation of disjunctive normal form may easily explode. Detection of duplicates helps in reducing the size of resulting formulas thus speeding up subsequent use of the state predicates. 5 The idea of abstract interpretation [2] is to map certain entities into another (abstract) domain where some considerations can be verified more easily. Abstraction must be faithful (every result derived in the abstract domain must be correct in the original domain) but not necessarily precise (there may be results that hold in the original domain but cannot be derived in the abstract domain). Loss of precision is the price to be paid for easier approaches in the abstract domain.
We propose to use the set Z of integer numbers as abstract domain. We aim
at assigning a number abstr( ) to every state predicate such that the following
results may be reliably derived:
– if abstr(
We explicitly store abstr( ) for every state predicate and every of its subformulas. Hence, once computed, abstr( ) can be derived from in constant time. 6 In this section, we discuss the assignment of abstract values to atomic state predicates (all but the Boolean combinations). The following assignment reflects the frequent occurrence of certain propositions. Without loss of generality, we assume that P = fp1; : : : ; pmg and T = ft1; : : : ; tng.
– abstr(TRUE) := 1; – abstr(FALSE) := 1; – abstr(DEADLOCK) := 2; – abstr(INITIAL) := 3; – for all pi 2 P , abstr(pi > 0) := 3 + i and abstr(pi = 0) := – for all tj 2 T , abstr(FIREABLE(tj )) := m + 3 + j. 3 i;
For the remaining atomic propositions, we assign consecutive numbers. To this end, we introduce a “function” new() that returns, whenever called, a fresh (previously unused) number greater than 3 + m + n. That is, if any comparison, except the ones just mentioned, is used twice in a state predicate, the two incarnations get different values (and we do not detect their equality). – abstr(k1p1 + + knpn
k0) := new();
For soundness, it is important that indeed every call to new() returns a distinct value. In a threaded context, this can be achieved without synchronisation: let every call to new() in thread k of an n-threaded program return only values that are congruent to k modulo n. Obviously, the proposed setting meets the requirements mentioned in Section 5.
For simplicity, we consider only conjunction, disjunction, and negation. We basically assume that equivalence and implication leave the scene early in the game using well-known rewrite rules. Negation can be handled quite easily. abstr(: ) can be naturally set to abstr( ), so the value can be inherited from the subformula.
Next we consider a conjunction with k sub-formulas. We proceed inductively, starting with a conjunction that has 0 sub-formulas. During this process, we combine the definition of the abstract value of the conjunction with the detection of duplicates among the subformulas. An empty conjunction is treated as TRUE, so it receives abstract value 1. Assume that we want to add i to a given conjunction C = 1 ^ ^ i 1. We distinguish the following cases: – abstr(C) = 1: Then abstr(C ^ i) := abstr( i), and 1; : : : ; i 1 are removed from the formula; – abstr(C) = 1: Then abstr(C ^ i) := 1, and i is not added to the list of subformulas of C; – abstr( i) = 1: Then abstr(C ^ i) := abstr(C), and i is not added to the list of subformulas of C; – abstr( i) = 1: Then abstr(C ^ i) := 1, and 1; : : : ; i 1 are removed from the formula; – abstr(C) = abstr( i): Then abstr(C ^ i) := abstr(C), and i is not added to the list of subformulas of C; – abstr(C) = abstr( i): Then abstr(C ^ i) := 1; – There is a j < i with abstr( j ) = abstr( i). Then abstr(C ^ i) := abstr(C), and i is not added to the list of subformulas of C; – There is a j < i with abstr( j ) = abstr( i). Then abstr(C ^ i) := 1; – Otherwise, abstr(C ^ i) := new().
The assignment reflects simple laws of Boolean logic: ^ is and ^: is false. Hence, the assignment reflects the specification in Section 5. The approach relies on the assumption that formulas are constructed only by adding sub-formulas. It does not work for a process that involves the removal of a sub-formula.
For a disjunction, the assignment can be naturally derived from the considerations for conjunction and negation: 1 _ 2 is equivalent to :(: 1 ^ : 2). In particular, the empty disjunction should get value -1.
Using the above definition, the abstract value may depend on the order in
which subformulas appear in a conjunction or disjunction. Assuming abstr(
The described process can be used for updating abstract values while composing a formula from its constituents. This is the case for the original construction of the predicate, but also for the construction of a disjunctive normal form. There are a few constructions where we assign the abstract value differently. When we copy a predicate (for instance when rewriting an equivalence), the copy gets the same abstract value as the original predicate. When we transform a FIREABILITY, DEADLOCK, or INITIAL predicate into a Boolean combination of inequations, the resulting predicate inherits the abstract value of the original formula as well. When we turn a predicate into its negation (e.g. when applying de Morgan’s rule for eliminating negation symbols), the resulting predicate gets the inverse of the original value. 8
Consider the formula p = 1 () q = 0 where p and q are assumed to be places. Internally, we support only , so we would rewrite the formula to (p 1 ^ 1 p) () q 0 (assume that we detect q 0 to be a tautology since q cannot get a negative number of tokens). Further, we normalise the formula such that only ^ and _ is used. We apply the rewrite rule that replaces A () B with (A _ :B) ^ (:A _ B). We obtain: ((p 1 ^ 1 p) _ 1 q) ^ (p 0 _ 2 p _ q 0) This is the formula that we normally use for state space verification. Since the rewrite rule introduced copies of A and B, the two copies (and their subformulas) get the same value which is than inversed through negation in one of the two copies. This way, we preserve some knowledge about the origin of sub-formulas.
If, subsequently, we want to include the state equation (i.e. linear programming) approach, we transform the formula into a disjunctive normal form since linear program can handle only conjunctions of inequations. We proceed by first transforming the left part, resulting in (p 1 _ 1 q) ^ (1 p _ 1 q) ^ (p 0 _ 2 p _ q 0) Then we apply the law of distributivity to the whole formula. Doing that in the brute-force way, would result in in a disjunction of 12 subformulas: (p (p (p (p (p (p (1 (1 (1 (1 (1 (1 1 ^ 1 1 ^ 1 1 ^ 1 1 ^ 1 1 ^ 1 1 ^ 1 q ^ 1 q ^ 1 q ^ 1 q ^ 1 q ^ 1 q ^ 1 p ^ p p ^ 2 p ^ q q ^ p q ^ 2 q ^ q p ^ p p ^ 2 p ^ q q ^ p q ^ 2 q ^ q 0)_ p)_ 0)_ 0)_ p)_ 0)_ 0)_ p)_ 0)_ 0)_ p)_ 0) Our abstraction, however, recognises that p 0 is the negation of 1 p, p 1 is the negation of 2 p, and q 0 is the negation of 1 q since the abstraction of one the the formulas is 1 times the abstraction of the other one. The detection does not depend on the simplicity of these formulas since the abstraction takes care of copying and negation in the process of transforming the original formula. As soon as a formula and its negation appear in a conjunction, the conjunction is replaced by false and thus disregarded in the resulting formula. This way, first, second, 5th, 6th, 7th, 9th, and 12th subformulas Furthermore it recognises the duplicate appearance of 1 q in the 10th and 11th sub-formulas, so we would produce the normal form Our approach reduced a formula with 36 literals to a formula with 13 literals. Instead of 12 conjunctions, only 5 conjunctions need to be shipped to the linear programming tool. One might argue that formula would not have exploded in the first place if the equivalence A () B would have been rewritten by (A ^ B) _ (:A ^ :B). Using that rule, however, the negated formula would explode instead, so the choice of the rule for rewriting equivalence does not solve the problem of duplication. 9
We implemented the abstract interpretation in our tool LoLA 2 [5, 7]. Our main focus was to reduce the size of disjunctive normal form generation which is a pre-requisite for applying the state equation based method of [6]. The abstract interpretation yields a sufficient condition that sub-formulas can be merged. We jointly apply a hash-based technique that yields a sufficient condition for subformulas to be at least syntactically different. Whenever none of the two criteria applies, we investigate the sub-formulas recursively to look for additional duplicates. The abstract interpretation costs virtually no time, so we are convinced that it establishes a nice tool for handling state predicates in verification. Using special codes for frequently occurring atomic predicates, the method is in fact Petri net specific.