Deciding Detectability for Labeled Petri Nets ?
Tomáš Masopust a and Xiang Yin b
a Institute

of Mathematics, Czech Academy of Sciences, Žižkova 22, 616 62 Brno, Czechia

arXiv:1802.02087v1 [cs.LO] 6 Feb 2018

b Department

of Automation, Shanghai Jiao Tong University, Shanghai 200240, China

Abstract
Detectability of discrete event systems (DESs) is a property to determine a priori whether the current and subsequent states can be
determined based on observations. In this paper, we investigate the verification of two detectability properties – strong detectability and
weak detectability – for DESs modeled by labeled Petri nets. Strong detectability requires that we can always determine, after a finite
number of observations, the current and subsequent markings of the system, while weak detectability requires that we can determine, after
a finite number of observations, the current and subsequent markings for some trajectories of the system. We show that for DESs modeled
by labeled Petri nets, checking strong detectability is decidable whereas checking weak detectability is undecidable. Our results extend
the existing studies on the verification of detectability from finite-state automata to labeled Petri nets. As a consequence, we strengthen a
result on checking current-state opacity for labeled Petri nets.
Key words: Discrete event systems; Petri nets; Detectability; Opacity; Decidability

1

Introduction

State estimation is one of the central problems in the systems
and control theory. It plays a key role in many problems
where one needs to estimate the state of the system based
on imperfect observations. In this paper, we investigate an
important property in the state estimation problem, called
detectability, for discrete event systems (DESs) modeled by
labeled Petri nets.
In the context of DESs, the problem of state estimation has
been extensively investigated due to its applications in many
different problems [12,14,20]. In particular, Shu and Lin [20]
proposed the concept of detectability that characterizes a priori whether or not the current and subsequent states of a DES
modeled by a finite-state automaton can be determined based
on observations. The property of detectability has drawn a
considerable attention in the literature [10,17,18,24], including the complexity studies on the verification of different notions of detectability [11,27,28] and the generalization of the
notion to, e.g., stochastic discrete-event systems [9,10,24].
In this paper, we investigate the verification of two detectability properties – strong and weak detectability – in the context
? This paper was not presented at any conference. Corresponding
author X. Yin. Tel. +8613636434613. Fax +862134204522.
Email addresses: masopust@math.cas.cz
(Tomáš Masopust), yinxiang@sjtu.edu.cn (Xiang Yin).

Preprint submitted to Automatica

of the work of Shu and Lin [20] generalized from finite-state
automata to unbounded labeled Petri nets systems. Specifically, we assume that both the Petri net structure and the initial marking are known, and that the system is only partiallyobserved via a labeling function. Strong detectability then
requires that we can always determine, after a finite number of observations, the current and subsequent markings of
the system, whereas weak detectability requires that we can
determine, after a finite number of observations, the current
and subsequent markings
For systems modeled by finite-state automata, strong detectability can be verified in polynomial-time [17] whereas
checking weak detectability is a PSPACE-complete problem [27,28] even for a very restricted type of automata [11].
Consequently, both of these two properties are clearly decidable for bounded Petri nets since we can explicitly enumerate the reachable markings and then use the verification
techniques for automata. However, whether these properties
are decidable for unbounded Petri nets is no longer straightforward because the reachable space is infinite in general,
and, to the best of our knowledge, these problems are open.
In this paper, we resolve these questions. We first show that
verifying strong detectability for unbounded Petri nets is decidability by reducing the strong detectability verification
problem to a model checking problem for Yen’s logic [23,1].
As a second result, we show that checking weak detectability for unbounded Petri nets is undecidable. We prove the

7 February 2018

2

result by reducing the language inclusion problem for labeled Petri nets to the weak detectability verification problem. As a consequence of our construction, we strengthen
a result concerning the verification of current-state opacity
for labeled Petri nets.

Preliminaries and Definitions

We assume that the reader is familiar with the basic notions
of Petri nets [13]. For a set A, | A| denotes the cardinality
of A. An alphabet Σ is a finite nonempty set the elements
of which are called events. A word over Σ is a sequence of
events of Σ. Let Σ∗ denote the set of all finite words over Σ,
where the empty word is denoted by ε, and let Σω denote
the set of all infinite words over Σ. For a word u ∈ Σ∗ , |u|
denotes its length. Let N = {0, 1, 2, . . .} denote the set of all
non-negative integers.

Our work is related to several works on state estimation of
Petri nets [2,8,15,16,21]. In particular, it is closely related to
the work of Giua and Seatzu [8] who proposed several different observability properties for (unlabeled) place/transition
nets. Specifically, they proposed two observability properties
– marking observability and strong marking observability;
the former requires that there exists a word under which the
marking of the system can be precisely determined, while
the latter requires that the marking of the system can be precisely determined after a finite delay k.

A Petri net is a structure N = (P, T, Pre, Post), where P
is a finite set of places, T is a finite set of transitions such
that P ∪ T , ∅ and P ∩ T = ∅, Pre : P × T → N and
Post : P × T → N are the pre- and post-incidence functions
specifying the arcs directed from places to transitions and
vice versa, respectively. A marking is a function M : P →
N that assigns to each place of a Petri net a number of
tokens. A Petri net system (N, M0 ) is the Petri net N with the
initial marking M0 . A transition t is enabled in a marking
M if M(p) ≥ Pre(p, t) for every place p ∈ P. An enabled
transition t can fire and the resulting marking M 0 is defined
as M 0(p) = M(p) − Pre(p, t) + Post(p, t) for every p ∈ P.
σ
We write M −→ N to denote that the sequence of transitions
σ = t1 · · · tk is enabled in the marking M of a Petri net N,
σ
and M −→ N M 0 to denote that the firing of the sequence
of transitions σ results in a marking M 0. For the sake of
simplicity, we often omit the subscript N if the net is clear
σ
from the context. We write L(N, M0 ) = {σ ∈ T ∗ | M0 −→}
to denote the set of all transition sequences enabled in the
marking M0 .

Marking observability and strong observability are similar
(but not identical) notions to weak and strong detectability,
respectively. The main difference between our results and
the results of Giua and Seatzu [8] is that labeled Petri nets
are more general than the unlabeled models used by Giua
and Seatzu [8], which is also reflected in the results – we
show that weak detectability for labeled Petri nets is undecidable whereas Giua and Seatzu show that marking observability for their unlabeled models is decidable. Moreover,
in the case of strong marking observability, there is a given
pre-specified detection bound k. Therefore, this property is
trivially decidable by explicitly enumerating the reachable
markings of the system within k steps. Notice that we do not
pre-specify any such detection bound for checking strong detectability, which makes the verification of strong detectability for unbounded Petri nets non-trivial because the search
space is infinite in general.

A marking M is reachable in the Petri net system (N, M0 ) if
σ
there is a sequence of transitions σ ∈ T ∗ such that M0 −→ M.
The set of all markings reachable from the marking M0
defines the reachability set of the Petri net system (N, M0 ),
denoted by R(N, M0 ).

Our study is also related to the work of Ramírez-Treviñ et
al. [15] who proposed marking detectability. This property
is closely related to strong detectability. However, RamírezTreviñ et al. [15] only provide sufficient conditions for checking marking detectability. To the best of our knowledge,
(un)decidability of checking strong and weak detectability
in the context of Shu and Lin [20] for labeled Petri nets has
not yet been established in the literature.

A labeled Petri net system is a quadruple G = (N, M0, Σ, `),
where (N, M0 ) is a Petri net system, Σ is an alphabet (a set
of labels), and ` : T → Σ ∪ {ε} is a labeling function that
assigns to each transition t ∈ T a symbol from Σ ∪ {ε}. The
labeling function can be naturally extended to ` : T ∗ → Σ∗ by
defining `(σt) = `(σ)`(t) for σ ∈ T ∗ and t ∈ T; we further
define `(λ) = ε for the empty transition λ. We say that a
transition t ∈ T is observable if `(t) ∈ Σ; otherwise, it is
unobservable. The language of G is defined as the set L(G) =
{`(σ) | σ ∈ L(N, M0 )}. Similarly, we denote by L ω (G) the
set of all infinite words generated by G. For a word s ∈
L(G), we denote by R(G, s) = {M | σ ∈ L(N, M0 ), `(σ) =
σ
s, M0 −→ M } the set of all reachable markings consistent
with the observation s.

Finally, we would like to point out that detectability is a
property that determines a priori whether the marking of the
system can be detected. On the other hand, there is also a
large body of literature on the online marking estimation for
Petri nets. This topic is, however, beyond the scope of this
paper; an interested reader is referred to the literature [2,5,7]
for more details.
The rest of this paper is organized as follows. Necessary
preliminaries are introduced in Section 2. Decidability of
checking strong detectability for labeled Petri nets is shown
in Section 3, including its EXPSPACE-hardness, and undecidability of checking weak detectability for labeled Petri
nets is shown in Section 4. Conclusions are formulated in
Section 5.

As usual when detectability is discussed [17], we make the
following two assumptions on the system G:

2

• for every p0 ∈ P 0 and every t1, t2 ∈ T with `(t1 ) =
`(t2 ) , ε, we define Pre k (p0, (t1, t2 )) = Pre 0(p0, t2 ) and
Post k (p0, (t1, t2 )) = Post 0(p0, t2 );
• for every p k ∈ P k and every t k ∈ T k not in the above
four cases, we define Pre k (p k, t k ) = Pre k (p k, t k ) = 0,
that is, no arc is defined.

A1 G is deadlock free, that is, in every reachable marking
of the system, there is at least one transition that can
fire; and
A2 G cannot generate an infinite unobservable sequence.
3

Strong Detectability
Essentially, (N k, M0, k ) is constructed to track all pairs of
sequences that have the same observation. More specifically,
for any (σ, σ 0) ∈ L(N k, M0, k ), we have `(σ) = `(σ 0). On the
other hand, for any σ, σ 0 ∈ L(N, M0 ) such that `(σ) = `(σ 0),
there exists a sequence in (N k, M0, k ) whose first and second
components are σ and σ 0, respectively (possibly by inserting
the empty transition λ).

Strong detectability is a property requiring that we can determine, after a finite number of observations, the current
and subsequent states for all trajectories of the system. This
property is formally defined as follows.
Definition 1 (Strong detectability). A labeled Petri net system G = (N, M0, Σ, `) is strongly detectable if there exists
an integer n ≥ 0 such that for every infinite word s ∈ L ω (G)
and every finite prefix s 0 of s, if s 0 is longer than n, then
|R(G, s 0)| = 1.

The following result shows how to use the structure
(N k, M0, k ) to verify strong detectability.
Theorem 2. A labeled Petri net G = (N, M0, Σ, `) is not
strongly detectable if and only if there exists a sequence

In order to check strong detectability, it suffices to verify
whether or not there exist two arbitrarily long sequences
such that: (i) they have the same observation; and (ii) they
lead to two different markings.

β

α

γ

M0, k −−→ Nk M1 −−→ Nk M2 −−→ Nk M3

(1)

in (N k, M0, k ) such that

To formalize this idea, we adopt the twin-plant construction for Petri nets used in the literature to test diagnosability [4,26] and prognosability [25].

(M2 ≥ M1 ) ∧
Ü

Formally, let G = (N, M0, Σ, `) be a labeled Petri net, and
let G 0 = (N 0, M00, Σ, `) be a place-disjoint copy of G, that
is, N 0 = (P 0, T, Pre 0, Post 0) where P 0 = {p0 | p ∈ P} is
a disjoint copy of P and the functions Pre 0 and Post 0 are
adjusted in the natural way. Moreover, the copy G 0 has the
same initial marking as G, that is, M00 (p0) = M0 (p) for every
place p0 ∈ P 0.


M3 (p) < M3 (p0) ∨ M3 (p) > M3 (p0) .

(2)

p ∈P

Proof. (⇐) Suppose that there exists a sequence satisfying
(1) and (2). For i = 1, 2, 3, let Mi,1 and Mi,2 denote the
first and the second components of Mi , respectively, that
> M > ]> where the lengths of M
is, Mi = [Mi,1
i,1 and Mi,2
i,2
coincide and are equal to the number of places in G. Let α =
(α1, α2 ), β = (β1, β2 ), and γ = (γ1, γ2 ). By the construction
of N k , `(α1 ) = `(α2 ), `(β1 ) = `(β2 ), and `(γ1 ) = `(γ2 ).
Furthermore, either β1 or β2 is not the empty transition;
without loss of generality, we assume that β1 , λ.

Then we define a new Petri net that is essentially the (labelbased) synchronization of G and G 0,
(N k, M0, k ) = ((P k, T k, Pre k, Post k ), M0, k )

Let n ∈ N be an arbitrary natural number. We consider an
infinite sequence

where the set of places is P k = P ∪ P 0, the initial marking M0, k = [M0> M00> ]> is the concatenation of the initial
markings of G and G 0, the transitions T k = (T ∪ {λ}) × (T ∪
{λ}) \ {(λ, λ)} are pairs of transitions of G and G 0 without
the empty pair, and the functions Pre k : P k × T k → N and
Post k : P k × T k → N are defined as follows:

α1 β1m+1 γ1 w ∈ L ω (G)
where w is an arbitrary infinite continuation of the sequence
σ1 = α1 β1m+1 γ1 such that `(w) , ε; such a continuation
exists by the assumption that the system is deadlock-free and
that there does not exist an infinite unobservable sequence.
The sequence σ1 is well-defined in G because M1 ≤ M2 ,
and hence the sequence σ2 = α2 β2m+1 γ2 ∈ L(G) is also welldefined in G.

• for every p ∈ P and every t ∈ T with `(t) = ε, we
define Pre k (p, (t, λ)) = Pre(p, t) and Post k (p, (t, λ)) =
Post(p, t);
• for every p0 ∈ P 0 and every t ∈ T with `(t) = ε, we define Pre k (p0, (λ, t)) = Pre 0(p0, t) and Post k (p0, (λ, t)) =
Post 0(p0, t);
• for every p ∈ P and every t1, t2 ∈ T with `(t1 ) =
`(t2 ) , ε, we define Pre k (p, (t1, t2 )) = Pre(p, t1 ) and
Post k (p, (t1, t2 )) = Post(p, t1 );

σ1

σ2

Let M0 −−→ N Mσ1 and M0 −−→ N Mσ2 . Then
Mσi = Mi,3 + m · (Mi,2 − Mi,1 ) .

3

tloop

Let p be a place such that M3 (p) , M3 (p0). Then we can
always find an integer m ≥ n such that Mσ1 (p) , Mσ2 (p0).
Since s = `(α1 β1m+1 γ1 ) = `(α2 β2m+1 γ2 ) is a prefix of the sequence of labels `(α1 β1m+1 γ1 w), we have that {Mσ1 , Mσ2 } ⊆
R(G, s), and hence |R(G, s)| > 1. Moreover, we have that
|s| ≥ m + 1 > n. Since n was chosen arbitrarily, the system
is not strongly detectable.

pnew,3
G
p1

(⇒) To prove the other direction, suppose that the system is
not strongly detectable, that is,

pnew,2

(∀n ∈ N)(∃s ∈ L ω (G))(∃s 0 finite prefix of s)
h
i
|s 0 | ≥ n ∧ |R(G, s 0)| > 1 .

By (i) and the construction of N k , there exists a sequence
σ = (σ1, σ2 ) ∈ L(N k, M0, k ) such that σ1 = α and σ2 = β.
We write (σ1, σ2 ) = t1 t2 t3 · · · tk , where ti ∈ T k and k ≥
n. Let M1, M2, M3, . . . , Mk be the markings induced by the
transitions, that is,
t3

tk

where Mk = [Mα> Mβ> ]> . Notice that k can be arbitrarily
large by choosing n to be arbitrarily large. Since vectors of
natural numbers with the product order form a well-quasiordering, Dickson’s lemma [6] shows that there is no infinite
sequence of vectors M1, M2, M3, . . . such that Mi > M j for
every i < j. Therefore, choosing k sufficiently large implies
that there exist 1 ≤ i < j ≤ k such that Mi ≤ M j yielding a
sequence
ti+1 ···t j

t j+1 ···tk

M0, k −−−−→ Nk Mi −−−−−−→ Nk M j −−−−−−→ Nk Mk .

M(

pnew,1

p n)

Although Yen’s logic is decidable, its precise complexity
is open. There is a so-called increasing fragment of Yen’s
logic that among others requires that Mk ≥ M1 . Deciding
satisfiability of this fragment is EXPSPACE-complete [1].
However, the reader can see that this property is not satisfied
by our formula in Theorem 2, and hence the existing results
do not imply any upper bound complexity.

M0, k −
→ Nk M1 −
→ Nk M2 −
→ Nk · · · −→ Nk Mk

t1 ···ti

..
.

pn )

tuo,1

M(p2 )

Proof. Decidability comes from the fact that the existence of
a sequence satisfying the formula (2) is expressed by Yen’s
logic [23,1], whose satisfiability is decidable.


β

(ii) Mα , Mβ , where M0 −
→ N Mα and M0 −
→ N Mβ .

t2

M(

p1 )

Fig. 1. Sketch of the hardness construction

(i) `(α) = `(β) and |`(α)| = |`(β)| ≥ n; and

t1

p2

pn

This implies that, for any n ∈ N, there exist two sequences
α, β ∈ L(N, M0 ) such that
α

tuo,2

M(

p 1)
M(
M(p2 )

To discuss the lower bound complexity, we show that checking strong detectability requires at least exponential space.
Our approach is to reduce the coverability problem, which is
know to be EXPSPACE-complete, to the strong detectability
verification problem.
Theorem 4. Checking strong detectability is EXPSPACEhard.

(3)

Since Mk = [Mα> Mβ> ]> and Mα , Mβ , there exists a place
p such that Mk (p) = Mα (p) , Mβ (p0) = Mk (p0). Therefore, (3) satisfies the properties (1) and (2), which was to be
shown.


Proof. Given a Petri net system (N, M0 ), the coverability
problem asks whether there is a reachable marking that covers a given marking M.
Let (N, M0 ) and M be the instance of the coverability problem. We construct a new Petri net as follows (see Fig. 1 for
an illustration). We add two new unobservable transitions
tuo,1 and tuo,2 , and two new place pnew,1 and pnew,2 initialized with zero tokens to (N, M0 ), and we define

To state our first result, we briefly recall the notion of Yen’s
logic that allows us to test the existence of a sequence
σk
σ1
σ2
M0 −−→ M1 −−→ · · · Mk−1 −−→ Mk such that a predicate
φ(M1, . . . , Mk ) holds, where φ(M1, . . . , Mk ) is a marking
predicate obtained by conjunctions and disjunctions of terms
of the form of Mi (p) = M j (p0), Mi (p) > M j (p0) and Mi (p) <
M j (p0), for places p and p0. For more details on Yen’s logic,
the reader is referred to the literature [23,1].

(
Pre(p, tuo,1 ) = Pre(p, tuo,2 ) =
(
For i = 1, 2, Post(p, tuo,i ) =

Theorem 3. Checking strong detectability is decidable for
labeled Petri nets.

4

M(p)

if p ∈ P

0

otherwise

1

if p = pnew,i

0

otherwise

Then, we add a new isolated place pnew,3 initialized with
one token, and we define a new self-loop transition tloop
in pnew,3 . This guarantees that the system is deadlock-free.
Finally, we define the labeling function

p4 ) is connected by a self-loop to every transition of G1
(resp. G2 ). Intuitively, p1 (resp. p2 ) allows G to simulate G1
(resp. G2 ). For every place of G1 , we create a new transition
labeled by a to which the place is connected, and through
which there is a self-loop from place p2 back to place p2 .
The intuition is that p2 allows G to remove the tokens from
the G1 part under a word from a∗ . The rest of the Petri net
G is as depicted in Fig. 2.

` : T ∪ {tuo,1, tuo,2, tloop } → T ∪ {tloop }
by
(
`(t) =

t

if t ∈ T ∪ {tloop }

ε

if t ∈ {tuo,1, tuo,2 }

The initial marking of G is such that the G1 and G2 parts
contain the initial markings of G1 and G2 , and p0 contains a
single token. At the beginning, only the transitions connected
to place p0 are enabled. Then, after the first transition, the
net G either simulates G1 or G2 , and hence its ω-language is

By the construction, unobservable transitions tuo,1 and tuo,2
can be fired if and only if there exists a reachable marking
in the original Petri net that covers M. Thus, if these two
unobservable transitions are firable, then the modified system is not strongly detectable because we cannot distinguish
between the tokens in pnew,1 and pnew,2 . On the other hand,
if these two unobservable transitions are not firable, then
all firable transitions are observable, which directly implies
that the system is strongly detectable. Overall, the original
system has a reachable marking that covers M if and only if
the modified system is strongly detectable. Hence, deciding
strong detectability is EXPSPACE-hard.

4

{xwxay(w) bω | w ∈ L(G1 )}
∪ {xwx(aω + a∗ bω ) | w ∈ L(G2 )}
where y(w) is finite and depends on the number of tokes in
the net G1 after generating the word w ∈ L(G1 ).
If L(G1 ) * L(G2 ), then there exists a word w ∈ L(G1 ) −
L(G2 ). We now consider all markings of G1 after generating
the word w. There can be several, but a finite number of
such markings, because the length of w is finite and there
are no λ-transitions in G1 . We sum the tokes in every such
marking and let k denote its maximum. This means that after
generating xwxak b, the marking of G is such that a single
token is in place p3 , no token is in the part of G1 , because
k is the maximum number of tokes in G1 after generating
w, so we had to use all of them to generate ak , and the
part of G2 contains its initial marking. If the net now keeps
generating bω , we stay in this marking for ever. This is the
only marking reachable by the ω-word xwxak bω , because
w < L(G2 ). Thus, the net is weakly detectable; the n from
the definition is n = |xwx| + k + 1, which is a constant for
such a fixed word w.

Weak Detectability

In some applications, we only need to determine, after a
finite number of observations, the current and subsequent
states for some trajectories of the system. This property is
referred to as weak detectability and is formally defined as
follows.
Definition 5 (Weak Detectability). A labeled Petri net system G = (N, M0, Σ, `) is weakly detectable if there exists an
integer n ≥ 0 and a word s ∈ L ω (G) such that |R(G, s 0)| = 1
for any prefix s 0 of s of length at least n.

If L(G1 ) ⊆ L(G2 ), then any word xvxau bω generated using
the part with G1 , that is, v ∈ L(G1 ) and u is bounded by
the number of tokes in any marking of G1 reachable after
generating v in G1 , can be simulated using the part of G2 .
Moreover, any word generated by the part using G2 always
leads to at least two different markings; namely, a token is in
p6 (resp. p7 ) or in p8 (resp. p9 ), and hence it is not weakly
detectable.


Deciding weak detectability for DES modeled by finite-state
automata is a PSPACE-complete problem. We now show that
it is undecidable for DES modeled by unbounded Petri nets.
Theorem 6. Weak detectability is undecidable for labeled
Petri nets.
Proof. To prove our result, we reduce the inclusion problem
for labeled Petri nets that is known to be undecidable [?].
Let G1 and G2 be two labeled Petri nets. The problem asks
whether L(G1 ) ⊆ L(G2 ). Moreover, without loss of generality, we may assume that the labels of G1 and G2 do not
contain empty labels, that is, `(t) is not the empty word for
any transition t.

4.1

Application to Opacity

Opacity is another observational property related to the privacy and security analysis. The system has a secret modeled
as a set of markings and an intruder is modeled as a passive
observer with limited observation. The system is opaque if
the intruder never knows for sure that the system is in a
secret marking. We first recall the definition of opacity for
labeled Petri nets [3,22].

From G1 and G2 , we construct a labeled Petri net G as
follows. We create 10 new places p0 up to p9 , and we use
new labels x, a, and b as depicted in Fig. 2. Place p1 (resp.

5

p1

p2

p3

x

b

b

G1
x

a
b

a

p0

a

p8

x

a

p9
b

b

G2
p4

p5
x

a

b
p6

b
p7

a
b

Fig. 2. Sketch of the construction; labels are depicted in the transitions

Definition 7 (Current-State Opacity). Let G = (N, M0, Σ, `)
be a labeled Petri net system and S ⊆ R(N, M0 ) be a secret
set. System G is said to be current-state opaque with respect
σ
to S if for every M ∈ S and σ ∈ L(N, M0 ) such that M0 −→
0
0
M, there exists σ ∈ L(N, M0 ) such that `(σ ) = `(σ) and

However, we obtain this result as an immediate consequence
of the proof of Theorem 6.
Corollary 9. Single-marking current-state opacity for labeled Petri nets is undecidable.

σ0

M0 −−→ M 0 with M 0 < S.

Our result thus strengthens the result of Tong et al. [22] in
two directions:

A labeled Petri net system being current-state opaque means
that for every transition sequence σ leading to a marking
in the secret set, there exists another transition sequence
σ 0 whose firing leads to a non-secret marking, and the two
sequences produce the same observation `(σ) = `(σ 0). As
a consequence, when the intruder observes the behavior of
a current-state opaque labeled Petri net system, it cannot
conclude whether the current state is contained in the secret
or not.

(1) the secret set is a singleton, and
(2) undecidability is shown for deadlock-free labeled Petri
net systems.
5

Conclusion

In this paper, we investigated two detectability properties
for labeled Petri nets – strong and weak detectability. We
showed that whereas checking strong detectability is decidable, checking weak detectability is undecidable. As a consequence, we strengthened the undecidability result of checking current-state opacity to the case where the secret set is
a singleton and the Petri net is deadlock free.

Tong et al. [22] have shown that deciding whether a labeled
Petri net system is current-state opaque is an undecidable
problem. However, in their proof, they construct a system
with more than one secret marking. As a special case of
the current-state opacity problem, we define the following
single-marking current-state opacity.

Besides strong and weak detectability properties, there
are other notions of detectability proposed in the literature, such as initial-state detectability [19], generalized
detectability [17] or delayed detectability [18]. Investigating
the verification of these variants for labeled Petri nets is an
interesting future direction.

Definition 8 (Single-marking current-state opacity). Let
G = (N, M0, Σ, `) be a labeled Petri net system, and let
Ms ∈ R(N, M0 ) be a secret marking. System G is said to be
single-marking current-state opaque with respect to Ms if it
is current-state opaque with respect to the singleton {Ms }.
We point out that the proof of Tong et al. [22] does not
show that the single-marking current-state opacity problem
for labeled Petri nets is undecidable. Moreover, the Petri net
they construct in their proof is not deadlock-free.

Acknowledgements
T. Masopust was supported by RVO 67985840.

6

References

[23] H.-C. Yen. A unified approach for deciding the existence of certain
Petri net paths. Information and Computation, 96(1):119–137, 1992.

[1] M. F. Atig and P. Habermehl. On Yen’s path logic for Petri
nets. International Journal of Foundations of Computer Science,
22(4):783–799, 2011.

[24] X. Yin. Initial-state detectability of stochastic discrete-event systems
with probabilistic sensor failures. Automatica, 80:127–134, 2017.
[25] X. Yin. Verification of prognosability for labeled Petri nets.
IEEE Transactions on Automatic Control, 2018. To appear, doi:
10.1109/TAC.2017.2756096.

[2] F. Basile, M. P. Cabasino, and C. Seatzu. State estimation and
fault diagnosis of labeled time Petri net systems with unobservable
transitions. IEEE Transactions on Automatic Control, 60(4):997–
1009, 2015.

[26] X. Yin and S. Lafortune. On the decidability and complexity of
diagnosability for labeled Petri nets. IEEE Transactions on Automatic
Control, 62(11):5931–5938, 2017.

[3] J. Bryans, M. Koutny, and P. Y. A. Ryan. Modelling opacity
using Petri nets. Electronic Notes in Theoretical Computer Science,
121:101–115, 2005.

[27] X. Yin and S. Lafortune. Verification complexity of a class
of observational properties for modular discrete events systems.
Automatica, 83:199–205, 2017.

[4] M. P. Cabasino, A. Giua, S. Lafortune, and C. Seatzu. A new
approach for diagnosability analysis of Petri nets using verifier nets.
IEEE Transactions on Automatic Control, 57(12):3104–3117, 2012.

[28] K. Zhang. The problem of determining the weak (periodic)
detectability of discrete event systems is PSPACE-complete.
Automatica, 81:217–220, 2017.

[5] M. P. Cabasino, C. N. Hadjicostis, and C. Seatzu. Marking observer
in labeled Petri nets with application to supervisory control. IEEE
Transactions on Automatic Control, 62(4):1813–1824, 2017.
[6] L. Dickson. Finiteness of the odd perfect and primitive abundant
numbers with n distinct prime factors. American Journal of
Mathematics, 35(4):413–422, 1913.
[7] M. Dotoli, M. P. Fanti, A. M. Mangini, and W. Ukovich. On-line
fault detection in discrete event systems by Petri nets and integer
linear programming. Automatica, 45(11):2665–2672, 2009.
[8] A. Giua and C. Seatzu. Observability of place/transition nets. IEEE
Transactions on Automatic Control, 47(9):1424–1437, 2002.
[9] C. Keroglou and C. N. Hadjicostis. Detectability in stochastic discrete
event systems. Systems & Control Letters, 84:21–26, 2015.
[10] C. Keroglou and C. N. Hadjicostis. Verification of detectability in
probabilistic finite automata. Automatica, 86:192–198, 2017.
[11] T. Masopust. Complexity of deciding detectability in discrete event
systems. arXiv preprint:1710.02516, 2017.
[12] C. M. Ozveren and A. S. Willsky. Observability of discrete
event dynamic systems. IEEE Transactions on Automatic Control,
35(7):797–806, 1990.
[13] J. L. Peterson. Petri Net Theory and the Modeling of Systems.
Prentice Hall, NJ, USA, 1981.
[14] P. J. Ramadge. Observability of discrete event systems. In Conference
on Decision and Control (CDC), pages 1108–1112, 1986.
[15] A. Ramírez-Treviñ, I. Rivera-Rangel, and E. López-Mellado.
Observability of discrete event systems modeled by interpreted Petri
nets. IEEE Transactions on Robotics and Automation, 19(4):557–
565, 2003.
[16] Y. Ru and C.. Hadjicostis. Sensor selection for structural observability
in discrete event systems modeled by Petri nets. IEEE Transactions
on Automatic Control, 55(8):1751–1764, 2010.
[17] S. Shu and F. Lin. Generalized detectability for discrete event
systems. Systems & Control Letters, 60(5):310–317, 2011.
[18] S. Shu and F. Lin. Delayed detectability of discrete event systems.
IEEE Transactions on Automatic Control, 58(4):862–875, 2013.
[19] S. Shu and F. Lin. I-detectability of discrete-event systems. IEEE
Transactions on Automation Science and Engineering, 10(1):187–
196, 2013.
[20] S. Shu, F. Lin, and H. Ying. Detectability of discrete event systems.
IEEE Transactions on Automatic Control, 52(12):2356–2359, 2007.
[21] Y. Tong, Z. Li, and A. Giua. On the equivalence of observation
structures for Petri net generators. IEEE Transactions on Automatic
Control, 61(9):2448–2462, 2016.
[22] Y. Tong, Z. Li, C. Seatzu, and A. Giua. Decidability of opacity
verification problems in labeled Petri net systems. Automatica, 80:48–
53, 2017.

7

