Partial order reduction (POR) is a key technique to tackle the state explosion problem in the model checking (MC) domain. POR is based on the observation that concurrent and independent running processes contribute extensively to the state explosion problem, while having only little influence on the property preservation of individual processes. In essence, while building the state space, in each found state, POR methods compute a subset of transitions and only fire the transitions in it, to explore more states. Hence, the state space is reduced. The computed subset of transition has to satisfy certain requirements for property preservation. We propose a new POR method for linear temporal logic (LTL), which generalizes and extends ideas from [8]. LTL MC uses most commonly Büchi automata to represent the property under investigation. Compared to conventional LTL POR methods we exploit additional information available from the Büchi automaton. As a result, we are able to weaken or completely drop certain requirements and restrictions. For example the restriction to LTL X is dropped. We demonstrate the reduction efficiency on several examples.
Model checking (MC) is concerned with the question, whether a given model of a
system meets a given specification. Although there has been remarkable progress in
verifying properties over the years, the biggest issue for MC remains the state explosion
problem. In explicit MC one core technique to tackle large state spaces is the
reduction of the original state space to a smaller one. Example methods are symmetry [
POR appears to be the most powerful reduction technique. Our explicit model
checker LoLA 2 [
Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
POR is based on the observation that concurrent and independent running processes
contribute extensively to the state explosion problem, while they have little influence
on the property preservation of individual processes. There exist several approaches to
POR techniques: Ample Sets [
In conventional LTL MC with POR the state space is first reduced, and then,
together with the Büchi automaton of the (negated) formula, a product automaton is built,
where the actual verification takes place. In [
With the additional information available from the Büchi automaton, we propose a
new automata based POR, which is a generalization and extension of the ideas presented
in [
The paper is organized as follows. We start in Section 2 with a brief introduction of the terminology of P/T nets and LTL. Then we introduce LTL MC using Büchi automata in Section 3. Section 4 is concerned with the POR, more precisely the stubborn set method and the principles involved in the preservation of certain properties. In Section 5 we introduce our new automata based POR approach. We continue in Section 6 with a comparison between the conventional method and the new one. We conclude with some remarks regarding related work and some thoughts on future work in Section 7.
Definition 1 (Place/Transition Net). A place/transition net, P/T net for short, consists of a finite set of places P , a finite set of transitions T where P \ T = ;, a set of arcs F (P T ) [ (T P ), a weight function W : (P T ) [ (T P ) ! N where W (x; y) = 0 if and only if (x; y) 2= F , and an initial marking m0 : P ! N, where marking is a mapping m : P ! N.
The behaviour of a P/T net is defined by the transition rule.
Definition 2 (Transition rule of a P/T net). Let N = [P; T; F; W; m0] be a P/T net. Transition t 2 T is enabled in marking m if, for all p 2 P , W (p; t) m(p). If t is enabled in m, t can fire, producing a new marking m0 where, for all p 2 P , m0(p) = m(p) W (p; t) + W (t; p). This firing relation is denoted as m !t m0. It can be extended to a marking sequence, also called transition sequence, by the following inductive scheme: m !" m (for the empty sequence "), and m ! m0 ^ m0 !t m00 =) ! m !!t m00 (for a sequence ! 2 T and a transition t 2 T ).
Using the transition rule, a P/T net induces the reachability graph, also called the state space of the P/T net.
Definition 3 (Reachability graph of a P/T net). The reachability graph (M; E) of a P/T net N has a set of vertices M that comprises all markings that are reachable by any t sequence from the initial marking of N . Every element m ! m0 of the firing relation (t 2 T ) defines an edge E from m to m0 annotated with t.
Throughout the paper we are concerned with paths in the reachability graph. Definition 4 (Path, Suffix). Let (M; E) be the reachability graph of a P/T net. A finite path starting in state m1 is a sequence m1 : : : mn of states where, for all i < n, (mi; mi+1) 2 E. An infinite path starting in m1 is an infinite sequence m1m2 : : : where, for all i, (mi; mi+1) 2 E. A path is a finite or infinite path. A path is maximal if it is infinite, or is a finite path m1 : : : mn where mn is a deadlock, i.e. a state where, for all m 2 M , (mn; m) 2= E.
For self-containedness we continue with the introduction of the syntax and semantics of the temporal logic LTL, although we are using it mainly for the experimental validation. All results in this paper rely on Büchi automata as such.
Definition 5 (Syntax of LTL). TRUE, FALSE, DEADLOCK, FIREABLE(t) (for t 2 T ), and k1p1 + + knpn k (ki; k 2 Z; pi 2 P ) are atomic propositions AP . For a given set of AP , the temporal logic LTL is inductively defined as follows: – Every ' 2 AP is a state formula; – If ' and are state formulas, so are (' ^ ), (' _ ), and :'; – Every state formula is a path formula; – If ' and are path formulas, so are (' ^ ), (' _ ), :', X ', F ', G ', (' U ), and (' R ); Definition 6 (Semantics of LTL). A P/T net N satisfies an LTL formula ' if and only if every path ! = m m1m2 : : : in the reachability graph of N , satisfies ' according to the following inductive scheme: – ! j= TRUE, ! 6j= FALSE; – ! j= FIREABLE(t) if t is enabled in m; – ! j= DEADLOCK if there is no enabled transition in m; – ! j= k1p1 + + knpn k if k1m(p1) + + knm(pn) – ! j= :' if m 6j= '; – ! j= (' ^ ) if m j= ' and m j= ; – ! j= X' if m1 j= '; – ! j= 'U if there is exists a k 0 s.t. that mk j= mi j= '.
k; and, for all i with 0 i < k, The semantics of the remaining LTL operators is defined using the tautologies (' _ ) () :(:' ^ : ), F' () (TRUE U'), G' () :F :', and ('R ) () :(:'U: ).
LTL formulas can be stuttering invariant.
Definition 7 (Stuttering invariance). An LTL formula ' is stuttering invariant, if for all finite paths !1, all markings m and all infinite paths !2 it holds: !1m!2 j= ' () !1mm!2 j= '.
Stuttering invariant LTL formulas are exactly those formulas that do not contain the
X-operator [
jB'j
For self-containedness we also briefly introduce the standard definition of Büchi
automata, how they are used in MC, and their link to LTL. In [
Definition 8 (Büchi automaton). A Büchi automaton B = (Q; q0; ; ; QF ) consists of – a finite set Q of Büchi states – with q0 2 Q as its initial state, – a transition relation Q Q – with labelling function : !
a set of atomic propositions, – and a set QF Q of final states.
, where are propositional logic formulas over B accepts an infinite sequence of markings m1m2 : : : if and only if there is an infinite sequence q0q1 : : : s.t. – for all i, (qi; qi+1) 2 ; – for all i, mi+1 j= (qi; qi+1); – for infinitely many i, qi 2 QF .
The actual on-the-fly verification runs in the product automaton B , which is again a Büchi automaton. It is built from the system (M; E) and the Büchi automaton of the negated formula B:'.
Definition 9 (Product system). Let B = (Q; qs; ; ; QF ) be a Büchi automata and N be a P/T net with reachability graph (M; E). The product system (M; E) \ B is a Büchi automaton B = (Q ; q0 ; ; ; QF ) where – q0 is some element not contained in M Q, – Q = M Q [ fq0 g, – (q0 ; (m; q)) 2 iff (q0; q) 2 and m = m0 j= (q0; q), – ((m; q); (m0; q0)) 2 iff (m; m0) 2 E, (q; q0) 2 and m0 j= (q; q0), – (q ; q 0) = tt for all q ; q 0 2 , where tt is the formula which is always true, – (m; q) 2 QF iff q 2 QF .
The product automaton represents a combination of the current marking in the reachability graph and the current state of the Büchi automaton. It accepts exactly those infinite paths which violate the property '. This means that to verify an LTL formula ', we check whether there exists a path in B , which can be executed in (M; E). If we found such a path, also called counterexample, it follows that ' does not hold in the system.
Proposition 1 (LTL to Büchi automaton, [
And the property ' is satisfied in the system, if the product automaton B accepts the empty language.
Proposition 2 (Emptiness check, [
Note that also a reduced reachability graph can be used to construct the product automaton. I.e., MC with Büchi automata can be combined with other reduction techniques, e.g., POR. 4
Partial Order Reduction — the Stubborn Set Method
Partial order reduction (POR) is a technique to reduce the state space of a system,
while preserving certain properties. There exist different approaches to this topic:
Ample Sets [
Given is an arbitrary, fixed P/T net N = [P; T; F; W; m0] with reachability graph (M; E) and a property '. The stubborn set method aims at producing a subgraph (M 0; E0) of the original reachability graph (M; E), s.t. the evaluation of ' using (M 0; E0) yields the same truth value as the evaluation of (M; E). We first define a mechanism to restrict the set of transitions T in each marking m to a subset called stubborn set or stubborn(m).
Definition 10 (Stubborn set generator). Let N = [P; T; F; W; m0] be a P/T net with reachability graph (M; E). A function stubborn : M ! 2T is called stubborn set generator and produces the reduced reachability graph (M 0; E0), s.t. (m; m0) 2 E0 () m !t m0 for a transition t 2 stubborn(m). M 0 is the set of markings, which can be reached from the initial marking by only firing transitions from stubborn(m) in the marking m.
The way the stubborn set generator is defined, gives us the possibility to choose in
any marking any subset we want, there are no restrictions. This is certainly not useful
if a property is investigated, since a random choice would most certainly not preserve
the property. The goal would be to reduce the state space as much as possible, while
choosing the subset in a way that the property under investigation is preserved. For this,
a set of requirements, which we also call principles, were introduced in the literature.
Each requirement has a specific purpose for proving property preservation. In most
cases, we assume that there is a path in the full reachability graph (e.g., a witness path
or a counterexample for the property under investigation) and show that the reduced
system contains a path 0 that is equally fit w.r.t. the studied property. We first introduce
the requirements, using the same terminology as in [
The first principle is commutativity (COM for short). It is the heart of virtually all POR methods. It describes a specific independence between transitions in the stubborn set and transitions not in the stubborn set. The main purpose of COM is that 0 may execute transitions in another order than . The firing of transitions, which are not part of the stubborn set, can be deferred until later, without losing possible ongoing paths. The left side of Fig. 2 shows this situation.
Definition 11 (COM: The commutativity principle). stubborn(m) T satisfies the commutativity principle if, for all ! 2 (T n stubborn(m)) and all t 2 stubborn(m), m !!t m0 implies m t!! m0.
m t m000 ! ! m00 t m0 m t ! m0 t
The next requirement is the key transition principle (KEY for short). KEY ensures that there is an enabled transition which can be switched to the beginning of a transition sequence. The purpose of KEY (in connection with COM) is that 0 may contain transitions that are not occurring in . In more detail KEY states that there is a transition t in the stubborn set which is enabled before and after firing a transition sequence which is not part of the stubborn set. This is illustrated in the right side of Fig. 2, Definition 12 (KEY: The key transition principle). stubborn(m) T satisfies the key transition principle if in m no transition is enabled or it contains a transition t (a key transition) such that, for all ! 2 (T n stubborn(m)) , m !! m0 implies that t is enabled in m0.
Before we continue with the next requirement which is concerned with the property ' under investigation, we introduce the invisibility property. Transitions that can change the truth value of an atomic proposition occurring in ' are called visible. Transition which can not change any are called invisible. This means firing a sequence of invisible transitions will have no effect on the truth value of the property '. Definition 13 (Invisibility property). A transition t is invisible w.r.t. an LTL formula ' regarding a set of transitions T 0 T , if for all atomic propositions occurring in ', all markings m 2 M and all finite transition sequences ! 2 (T 0) it holds: (m !! m0 ^ m t!! m00) =) (m0 j= called visible w.r.t. ' regarding T 0.
()
m00 j= ). Otherwise the transition t is
Now we can introduce the visibility principle (VIS(') for short). With VIS, visible transitions in 0 appear in the same order as in , if they appear in 0.
Definition 14 (VIS: The visibility principle). stubborn(m) T satisfies the visibility principle for a property ' if stubborn(m) contains only invisible transitions w.r.t. ' regarding (T n stubborn(m)), or all transitions.
p1 t1 p2 p3 t2
VIS(') ensures the same ordering of transitions, but it can introduce stuttering. As an example assume that the property ' = F(p2 > 0) should hold in the P/T net from Fig. 3. Transition t1 can change the truth value of ', namely if t1 fires it produces one token on p2, and with this ' is satisfied. This means there are two valid stubborn sets in m0. The first one is ft2g which contains only invisible transitions and the second one is ft1; t2g. If we choose ft2g as stubborn set, we reach the same marking m0 again after firing t2. We could now choose infinitely often t2 as stubborn set, which results in stuttering. To avoid infinite stuttering we introduce the last requirement, the nonignoring principle (IGN for short). IGN is used to ensure that all transitions of are eventually occurring in 0. The concept behind this is that if marking m is the start of a cycle in the reachability graph, which results again in m, then in at least one marking m0 in the cycle all enabled transitions have to be explored. In other words stubborn(m) consists of all enabled transitions in m0 to possibly leave the cycle.
Definition 15 (IGN: The non-ignoring principle). stubborn satisfies the non-ignoring principle if every cycle in the reduced reachability graph contains a marking where all enabled transitions are explored.
There exist some more principles, but they are not needed for this paper. More
details regarding principles and property preservation are provided in [
Proposition 3 (Preservation of deadlocks, [
For the preservation of terminal strongly connected components (SCC), used for example in the verification of liveness properties, we need to avoid infinite stuttering and thus we need IGN.
Proposition 4 (Preservation of terminal SCC, [
With these two propositions we have almost all ingredients for the preservation of linear time properties, with which we are concerned in this paper. Next to COM, KEY, and IGN we also need to preserve the linear time property '. Furthermore, we have to restrict LTL to stuttering invariant formulas. We call the following proposition the conventional LTL X POR method.
Proposition 5 (Preservation of LTL X, [
As mentioned before, the stubborn set generator used in conventional LTL X is a
function stubborn : M ! 2T . This means the state space of the P/T net is first reduced
and then the product automaton is built with the reduced state space. Compared to this,
the authors in [
Automata based Partial Order Reduction for LTL
In this section we introduce our new Büchi automata based POR. It is a generalization
and extension of the ideas proposed in [
The representation of the formula is realized by the state transitions between the Büchi states. All considerations regarding the formula are done locally around the current Büchi state. To illustrate this, let us consider the example Büchi automaton from . . .
1 2 n q '1 '2 'h q1 q2 . . . qh 1 2 m
Fig. 4. If we are in state q, we restrict the scope of the formula to the self loop , and to the progressing formulas 'i; i 2 [1; h]. When we are in q, we do not care about all the other parts of the formula, i.e., j ; j 2 [1; n], and k; k 2 [1; m]. This brings us to the main principle for the reduction. We call it the not-leaving principle (NLG for short): all transition sequences, which do not use transitions from the stubborn set, cannot leave the current Büchi state.
To formalize this, let in the sequel N = [P; T; F; W; m0] be an arbitrary, fixed P/T net with reachability graph (M; E), and ' be an arbitrary LTL formula with its corresponding Büchi automaton B:' = (Q; q0; ; ; QF ). The formula ' can consists of several atomic sub-propositions . Let q 2 Q be a Büchi state and = (q; q) be the formula of the self loop q ! q. We call the self loop the retarding formula. Further let h be the number of outgoing arcs from q which are progressing to new Büchi states and let 'i, with 0 i h be the formulas of the outgoing arcs. We call such formulas the progressing formulas. Now we formalize the main principle for the reduction. Definition 16 (NLG: The not-leaving principle). stubborn(m; q) T satisfies the not-leaving principle if, for all i 2 [1; h] and for all ! 2 (T n stubborn(m; q))+, ! m ! m0 implies m0 6j= 'i.
It holds that no transition sequence, from the set of transitions which are not in the stubborn set, can satisfy a progressing formula. For example, assume the progressing formula is 'i = p < 1, which means that place p has less than one token on it. Then no transition that has p in its postset can be outside of the stubborn set, since it would change ' to true. With NLG some requirements from the conventional LTL X method can be weakened or even dropped, resulting in several advantages of the new stubborn set method.
Invisibility principle: Since all considerations regarding the formula are done locally around the current Büchi state, all other parts of the formula can be ignored. In fact, the invisibility property can be simplified. In the conventional method the influence on atomic sub-propositions regarding the result of the entire formula is dependent on the temporal progression and not further known. This means, the truth values of atomic sub-propositions must be preserved in both directions, (m j= () m0 j= ). Whereas in the automata based reduction all temporal operators are expressed in the state transitions of the Büchi automaton and with this, the influence of the atomic subproposition is determined. A satisfied formula allows a progression to another state q0, but has no influence on other state transitions. It follows that we can simplify the invisibility property to an implication, (m j= =) m0 j= ). This means that a transition, which changes from true to false, is not allowed, but a transition, which makes only truer, is allowed now.
Definition 17 (Semi-invisibility property). A transition t 2 T is called semi-invisible w.r.t. an LTL formula ' regarding a set of transitions T 0 T , if for all markings m 2 M , all finite transition sequences ! 2 (T 0) and all atomic sub-propositions of ' it holds: (m !! m0 ^ m t!! m00) =) (m0 j= =) m00 j= ). Otherwise the transition t is semi-visible with respect to regarding T 0.
As a consequence we can introduce also a weaker visibility principle, called the semi-invisibility principle (S-INV for short).
Definition 18 (S-INV: Semi-invisibility principle). stubborn(m; q) T satisfies the semi-invisibility principle for an LTL formula ', if all enabled transitions t 2 stubborn(m; q) are semi-invisible with respect to ' regarding (T nstubborn(m; q)), or all transitions t 2 (T n stubborn(m; q)) are semi-invisible with respect to ' regarding the empty set.
Non-ignoring principle and LTL X: Since the reduction is only applied within
a Büchi state, stuttering becomes irrelevant. Finite stuttering within a Büchi state does
not change the accepting behaviour, and infinite stuttering can always be avoided, if
this was possible in the original product automaton, due to the reduction principle.
As consequence, the non-ignoring principle can be dropped. Furthermore, due to the
irrelevance of stuttering, the restriction to LTL X can also be dropped. The introduced
method preserves the full class of LTL. Due to the additional information available
from the Büchi automaton and due to the fact, that the reduction is only applied to the
current Büchi state, we know, whether we are in a transient Büchi state or not. Transient
Büchi states can only happen in the initial state, when an atomic proposition is checked
without any temporal operators, or they appear as representation of X-operators of the
formula. In [
Key-transition principle: In accepting states infinite stuttering is possible and also desired. But we have to ensure that there always exists an enabled transition to prolong the path to an infinite path. Hence, KEY has to hold only in accepting states. If the current Büchi state is not accepting, then only transition sequences from the stubborn set can leave the current Büchi state. Since we are not in an accepting state, this implies that on the considered path we will change at some point in the future the Büchi state. It follows that in non-accepting states KEY does not has to hold, due to the fact that every transition sequence, which leaves the current Büchi state, always contains a transition from the stubborn set. This follows directly from NLG.
The drawback for the weakened or dropped requirements is that we have to uphold the main principle, that all transition sequences, which do not use transitions from the stubborn set, cannot leave the current Büchi state. Since the Büchi automaton for the LTL formula, compared to the transition system, is very small, we want to stay as long as possible in one Büchi state to achieve further reduction. This means that we want to avoid transitions which are progressing to the next Büchi state. As long as the progressing formulas 'i are not satisfied, we are staying in the same Büchi state and can reduce further. We are now ready to state the main result of this paper.
Theorem 1 (Büchi automata based partial order reduction). Given is a Büchi automaton B = (Q; qs; ; ; QF ) and a P/T net N = (P; T; F; W; ms) with reachable markings M . Further let stubborn : M Q ! 2T be a stubborn set generator which satisfies the following properties: 1. stubborn(m; q) satisfies COM 2. stubborn(m; q) satisfies S-INV with respect to 3. stubborn(m; q) = T or 8t 2 stubborn(m; q) : m !t m0 =) m j 0 = 4. stubborn(m; q) satisfies NLG 5. If q 2 QF , then stubborn(m; q) satisfies KEY
Here = (q; q) means the formula of the self loop q ! q, which is also called the retarding formula, and 8i 2 [1; h] : 'i = (q; qi); q 6= qi are the progressing formulas of the outgoing edges of q in B, where h is the actual number of outgoing edges.
There exists an infinite accepting path in the reduced product system P, which is generated by stubborn, if and only if there exists an infinite accepting path in the original product system P. from (m; q), s.t. m t0:::t!i mi.
Proof. =): The reduced state space P is a subsystem of the original state space P, this means accepting paths in P trivially imply the same accepting paths in P.
(=: Let 2 (M Q)1 be an infinite accepting path in P. Assume P has no infinite accepting path. We can separate in 1 2, s.t. 1 is the largest prefix, which can be executed in P. Let (m; q) be the last state in 1. Furthermore, let (mi; qi); i 2 N0 be the state sequence in 2 and t0t1 : : : the sequence of transitions, which induce 2 qs | ! (m; q) t!0 (m0; q0) t1:::t!i (mi; qi) } | } Since (m; q) is the last state in 1, it follows that t0 2= stubborn(m; q). Due to t0 2= stubborn(m; q), requirement 4 (NLG), implies that q = q0. We consider two cases. In the first one q lies in the accepting set of B and we do not change the Büchi state any more and in the second one the Büchi state is changed at least once more on the remaining path.
Case 1: 8i 2 N0 : qi = q:
All states in 2 remain in the same Büchi state q, i.e., 8i 2 N0 : qi = q. This means that q is in the accepting set of B and all markings in 2 satisfying the retarding formula
qs | ! (m; q) t!0 (m0; q) t1:::t!i (mi; q) } | }
We consider two sub-cases. In the first one we assume that there exists a transition ti in stubborn(m; q) and in the second one we assume that there is no such ti in stubborn(m; q).
Case 1.1: 9ti 2 stubborn(m; q):
Assume there is a transition ti with ti 2 stubborn(m; q). We choose the smallest such i, which means that m t0:::t!i mi with ti 2 stubborn(m; q) and t0; : : : ; ti 1 2= stubborn(m; q). Using requirement 1 (COM) we switch ti to the front of the path and it holds that m tit0:::ti !1 mi.
qs | ! (m; q) tit0:::ti !1 (mi; q) } | } The following two cases show that requirement 4 (NLG) implies that all transitions t0; : : : ; ti 1 are satisfying the retarding formula .
Case 1.1.1: ti is semi-invisible with respect to :
Requirement 2 (S-INV) ensures, if ti is semi-invisible regarding , then all states along the new path tit0 : : : ti 1 are satisfying .
Case 1.1.2: m 6j= :
Otherwise using requirement 2 all transitions t0; : : : ; ti 1 are semi-invisible regarding and together with the fact that requirement 3 ensures that ti satisfies , all states along the new path tit0 : : : ti 1 are satisfying .
In both cases 1.1.1 and 1.1.2 the path 1 is extended by one state, which has an infinite accepting continuation in P.
qs | ! (m; q) t!i (m0; q) t0:::ti !1 (mi; q) } | } s.t. m t t0:!:: is executable in N .
Case 1.2: @ti 2 stubborn(m; q):
Assume there is no transition ti 2 stubborn(m; q). Since q is in the accepting set of B, requirement 5 (KEY) ensures that there exists a key-transition t 2 stubborn(m; q), qs ! (ms; qs) ! (m; q) t! (m ; q) t0:!:: | {z1 } | {z2 }
It follows the same argumentation as in cases 1.1.1 and 1.1.2. The following two cases show that requirement 4 (NLG) implies that t0; : : : are all satisfying the retarding formula .
Case 1.2.1: t is semi-invisible with respect to :
Requirement 2 (S-INV) ensures, if t is semi-invisible regarding , then all states along the new path t t0 : : : are satisfying . Case 1.2.2: m 6j= :
Otherwise using requirement 2 all transitions t0; : : : are semi-invisible regarding and together with the fact that t 2 stubborn(m; q) and requirement 3 ensure that t satisfies , all states along the new path t t0 : : : are satisfying .
In both cases 1.2.1 and 1.2.2 the path 1 is extended by one state, which has an infinite accepting continuation in P .
qs | ! (m; q) t! (m0; q) t!0 (m0; q) :!:: {z1 } | {z2 }
This construction can now be repeated as often as necessary to get an infinite accepting path in P , contradicting the assumption, that 1 is the longest executable prefix.
Case 2: 9n 2 N0 9(mn; qn) : qn 6= q:
There exists a state (mn; qn) which is leaving the current Büchi state, qn 6= q. Let qn the first such state, then it holds that 8i < n : qi = q and mn j= 'j , for a j 2 [1; h]. Requirement 4 (NLG) ensures that there exists a ti where i 2 [0; n] with ti 2 stubborn(m; q). Using requirement 1 (COM) we switch ti to the front of the path.
m tit0:::ti !1 mi ti+1:::t!n mn
It follows the same argumentation as in cases 1.1.1 and 1.1.2. The following two cases show that requirement 4 (NLG) implies that all transitions t0; : : : ; ti 1 are satisfying the retarding formula .
Case 2.1: ti is semi-invisible with respect to :
Requirement 2 (S-INV) ensures, if ti is semi-invisible regarding , then all states along the new path tit0 : : : ti 1 are satisfying .
Case 2.2: m 6j= :
Otherwise using requirement 2 all transitions t0; : : : ; ti 1 are semi-invisible regarding and together with the fact that requirement 3 ensures that ti satisfies , all states along the new path tit0 : : : ti 1 are satisfying .
Hence it holds, that the extension m tit0:::ti !1 mi ti+1:::t!n is also an infinite accepting path in P , with the same traversed sequence of Büchi states, where at least one more state is executable in P . This construction can be repeated at most n-times, to find an infinite accepting path in which all transitions t0 : : : tn (possibly in a different order) are executable in P . Which means that the path leaves q and changes to qn. For the new Büchi state qn we can, according to case 1 or case 2, apply the construction again, s.t. an executable infinite accepting path in P is formed, contradicting the initial assumption on the choice of . 6
We compare the new automata based approach with the conventional LTL X method.
We demonstrate for each weakened requirement promising potential gains in reduction
efficiency. For simplicity, we assume that the different formulas 'i, which we want to
verify, are already negated. Some of the examples and their descriptions are inspired
by [
The restriction to stuttering invariant formulas is dropped. A model checker, using
the conventional LTL POR, had to turn off POR for those formulas that contain the
X-operator. It had to use standard brute force model checking in such situations. In
the 2019 edition of the MCC [
For the next examples consider the P/T net in Fig. 5. It models a system of n 2 N concurrent processes, where each process has one transition tj , with 1 j n, one pre place ij (input), and one post place oj (output). The state space consists of 2n markings with 2n2n edges.
tt q0 n V oj = 1 j=1 tt q1
Fig. 6. Büchi automaton for LTL formula '1 = F Vjn=1 oj = 1 .
As first example we are considering the LTL formula '1 = F corresponding Büchi automaton is shown in Fig. 6. The conventional visibility property based on definition 13 states that every transition is visible to '1, i.e., each transition tj produces a token on oj . This means, there is no reduction possible with the conventional LTL X POR and the reduced state space is the same as the original state space with 2n markings. The product automaton has 2n + 2 reachable states: the initial state, 2n states in Büchi state q0, and one state in Büchi state q1.
Vn j=1 oj = 1 . The
In the automata based approach every transition is semi-invisible in both Büchi states q0 and q1. The reason for this is that based on definition 18 we only care for the retarding formula and the retarding formula is always true. We see here the sizeable effect of the weakened visibility principle. In q0 every singleton set ftj g is a valid stubborn set, as long as oj does not contain a token. Without firing tj the Büchi state q0 cannot be left. And in addition to this, all other transitions are independent of each other. The reduced product automaton has n + 3 reachable states: the initial state, n + 1 chain-shaped states in Büchi state q0, and one state in Büchi state q1. The exponential reduction from 2n + 2 to n + 3 states is based solely on the restriction of the visibility. n V oj = 0 j=1 q0 n W oj = 1 j=1 n W oj = 1 j=1 q1 Fig. 7. Büchi automaton for LTL formula '2 = Vjn=1 oj = 0 U
G
Wjn=1 oj = 1 .
The second LTL formula '2 = Vjn=1 oj = 0 U G Wjn=1 oj = 1 we are considering, has the corresponding Büchi automaton shown in Fig. 7. Again, every transition in '2 is visible based on definition 13 and as such no reduction can be applied using the conventional method. The product automaton has 2n + 1 reachable states: the initial state, one state in Büchi state q0, and 2n 1 states in Büchi state q1.
Using the new approach there is also no reduction possible in q0 based on the semiinvisibility principle, since every transition can leave the current Büchi state. But we can reduce in q1, due to fact that all transitions are semi-invisible. With this, every singleton stubborn set consisting of tj is valid, as long as oj is empty. The reduced product automaton has n(n+1) + 2 reachable states: the initial state, one state in Büchi 2 state q0, and n(n+1) states in Büchi state q1. Due to the scope restriction of the semi2 invisibility property, we only have a quadratic number of states instead of an exponential number of states.
tt q0
n i1 = 2 ^ iV=2 oj = 1 tt q1 Fig. 8. Büchi automaton for LTL formula '3 = F i1 = 2 ^ Vjn=2 oj = 1 . The LTL formula '3 = F i1 = 2 ^ Vn
j=2 oj = 1 is the third example we are considering and has the corresponding Büchi automaton shown in Fig. 8. The conventional definition of the visibility property (13) states that t1 is invisible to '3 w.r.t. T and that all other transitions t2; : : : ; tn are visible to '3 w.r.t. the empty set. This means in the initial state we can reduce T to the valid stubborn set ft1g. As consequence the state space is reduced to 2n 1 + 1 markings. And the product automaton is also reduced to 2n 1 + 2 reachable states: the initial state, and 2n 1 + 1 states in Büchi state q0. Note that in q1 no state is reachable, since i1 = 2 can never be satisfied.
With the automata based approach we can use requirement 5 (KEY) to get a substantially better reduction. Requirement 5 states that only in an accepting Büchi state an activated transition has to be in the stubborn set. We use the fact that q0 is not an accepting state and with this the empty set is a valid stubborn set. Although there are activated transitions in the initial state, with none of them it is possible to leave Büchi state q0. As mentioned before, the reason for this is that i1 = 2 can never be satisfied. Independent from n, the reduced product automaton has always two states: the initial state, and one state in q0. This extreme reduction power from 2n 1 + 2 to 2 states is based on the requirement, that the KEY principle only has to hold in accepting states. tt q0 tt tt tt q1 tt q0 (a) Unfavourable Büchi automaton
(b) Simplified Büchi automaton
One thing that should be mentioned is that the reduction power strongly dependents on the formula and the used Büchi automaton. With some effort we can construct unfavorable Büchi automata where the conventional LTL X POR performs better or equally good. Fig. 9 (a) shows such an unfavorable Büchi automaton for the LTL formula '4 = false. It accepts every path. The problem is that in every arbitrary state of the product automaton it is possible to switch between the Büchi states and with this, no reduction can be applied based on the retarding formula. Although every transition is invisible and thus independent of other transitions, we cannot exploit that in this case.
The product automaton with conventional POR has a size of 2n + 3 states, while the product automaton built with the new approach has 2 2n + 1 states. The good news is, the LTL formula '4 = false can also be represented with only one Büchi state, where simply one Büchi state from Fig. 9 (a) is removed, resulting in Fig. 9 (b). With this Büchi automaton the problem vanishes and the reduction power is identical for methods. Both have n + 2 states in the product automaton. We conclude that the newly introduced POR can substantially increase the reduction efficiency. Table 1 summarizes the advantages and disadvantages once again.
Property/principle
Old
New stubborn set generator M ! 2T M Q ! 2T X-operator not supported improved: supported VIS 3 improved: replaced by weaker S-INV IGN 3 improved: not required KEY 3 improved: required only in accepting states NLG not required 3
Most POR approaches for LTL are focusing on the reduction of the transition system
and omitting the additional information available from the Büchi automaton. To the
best of our knowledge, there exist two other approaches that uses information from
the Büchi state. First, in [
Our contribution is a generalization and extension of the ideas presented in [
With this, some requirements can be weakened or even dropped, resulting in several
advantages over the conventional POR. One drawback of the conventional approach is
that it only works on stuttering invariant formulas, that is, formulas which are not
containing the X-operator. In [
All in all we have weakened or dropped several requirements compared to other POR methods. We showed with examples, which involved some of the weakened or dropped requirements, the reduction efficiency. Compared to conventional methods the reduction power can be extremely better, e.g., n + 3 vs. 2n + 2 states, or 2 vs. 2n 1 + 2 states. The reduction power depends on the formula, or to be exact, on its corresponding Büchi automaton.
In future works we want to expand our new method to other formalisms than P/T
nets. Furthermore, we want to explore whether the new automata based approach can be
tuned to be always better or at least equally good as the conventional POR. In addition to
this, we want to implement our new method in our explicit model checker LoLA 2 [