PN-unsolvable words

The behavioural specification of a given concurrent system can be described in a form of a labelled transition system. One of the challenging tasks of system analysis is to construct a model of a system with exactly the same behaviour. Region theory provides an algorithm synthesizing a Petri net which reachability graph is precisely the given lts. Unfortunately, since the lts may be extremely large, the process of synthesis may be remarkably time consuming, as it is based on solving a great amount of linear equations. It seems reasonable to investigate certain classes of labelled transition systems in hope of obtaining more efficient (and also deterministic) algorithm of solving them, or at least of deciding whether a given lts is synthesizable. That is why the set of finite words over a binary alphabet which are Petri net solvable are considered here. Computer tests greatly eases the analysis of such systems. The files containing synthesizable and non-synthesizable binary words are given below.

Basic notions

A finite labelled transition system with initial state is a tuple TS = (S, →, T, s₀), where S is a finite set of nodes (states), T is a set of edge labels, →⊆(S × T × S) is a set of edges, and s₀ ∈ S is an initial state. A label t is enabled at s∈S, written formally as s[t⟩, if ∃s'∈S: (s,t,s')∈ →. A state s' is reachable from s through execution of σ∈T^*, denoted by s[σ⟩s', if there exists a directed path from s to s' whose edges are labelled consecutively by σ.

A word w∈Σ of length n uniquely corresponds to a finite transition system:

An initially marked Petri Net is denoted as N=(P,T,F,M₀), where P is a finite set of places, T is a finite set of transitions, F:((P×T)∪(T×P))→N is the flow function specyfying the arc weights, and M₀ is the initial marking (a mapping M:P→N indicating the number of tokens in each place). A transition t∈T is enabled at a marking M, denoted by M[t⟩, if ∀p∈P M(p)≥F(p,t). The firing of t leads from M to M', denoted M[t⟩M', if M[t⟩ and M'(p)=M(p)-F(p,t)+F(t,p). We can extend the notion to M[σ⟩M' for sequences σ∈T^*, and [M⟩ denotes the set of markings reachable from M.

The reachability graph RG(N) is the labelled transition system with the set of vertices [M₀⟩, the initial state M₀, the label set T, and the set of edges {(M,t,M') | M,M'∈[M₀⟩∧M[t⟩M'}. We say that a Petri Net N solves a labelled transition system TS, if the reachability graph of N is isomorphic to TS.

We say that a word w (linear LTS) is PN-solvable, if there exists a Petri Net N, which solves w. We say that a word w is PN-unsolvable, it there is no Petri Net solving w. A PN-unsolvable word w is called minimal, if w does not contain any proper factor, which is PN-unsolvable.

Algorithm

To generate the set of all minimal PN-unsolvable words of given length n≥0 we used the following algorithm.

• For each word c₁w∈X_n-1 (c₁∈Σ)
  • For each letter c₂ in alphabet Σ
    • If c₁wc₂ is PN-solvable ⇒ insert c₁wc₂ into X_n
    • Else (if c₁wc₂ is PN-unsolvable and wc₂ is PN-solvable) ⇒ insert c₁wc₂ into Y_n
• Return Y_n

To check PN-solvability of a word (linear LTS) we used synet.

Files

• Minimal binary PN-unsolvable words (up to length 110)
• Minimal binary PN-unsolvable words with separation points marked (up to length 110)
• Minimal binary PN-unsolvable words (each length in a separate file)
• Binary PN-solvable words (up to length 60)
• Binary PN-solvable words (each length in a separate file)
• Binary words PN-solvable without side-conditions (up to length 36)
• Binary words PN-solvable only with side-conditions (up to length 36)