Compiling Petri Net Mutual Reachability in Presburger

2025-04-29 0 0 337.88KB 25 页 10玖币

侵权投诉

arXiv:2210.09931v1 [cs.LO] 18 Oct 2022

Compiling Petri Net Mutual Reachability in

Presburger

Jérôme Leroux

Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400 Talence, France

jerome.leroux@labri.fr

Abstract

Petri nets are a classical model of concurrency widely used and studied in formal veriﬁcation with

many applications in modeling and analyzing hardware and software, data bases, and reactive

systems. The reachability problem is central since many other problems reduce to reachability

questions. The reachability problem is known to be decidable but its complexity is extremely high

(non primitive recursive). In 2011, a variant of the reachability problem, called the mutual reach-

ability problem, that consists in deciding if two conﬁgurations are mutually reachable was proved

to be exponential-space complete. Recently, this problem found several unexpected applications in

particular in the theory of population protocols. While the mutual reachability problem is known

to be deﬁnable in the Preburger arithmetic, the best known upper bound of such a formula was

recently proved to be non-elementary (tower). In this paper we provide a way to compile the mutual

reachability relation of a Petri net with dcounters into a quantiﬁer-free Presburger formula given

as a doubly exponential disjunction of O(d) linear constraints of exponential size. We also provide

some ﬁrst results about Presburger formulas encoding bottom conﬁgurations.

2012 ACM Subject Classiﬁcation Theory of computation →Logic and veriﬁcation

Keywords and phrases Petri nets, Vector addition systems, Formal veriﬁcation, Reachability prob-

lem

Funding Jérôme Leroux: The author is supported by the grant ANR-17-CE40-0028 of the French

National Research Agency ANR (project BRAVAS)

1 Introduction

Petri nets are a classical model of concurrency widely used and studied in formal veriﬁcation

with many applications in modeling and analyzing hardware and software, data bases, and

reactive systems. The reachability problem is central since many other problems reduce

to reachability questions. Unfortunately, the reachability problem is diﬃcult for several

reasons. In fact, from a complexity point of view, the problem was recently proved to be

Ackermannian-complete ([17] for the upper-bound and [5, 15] for equivalent lower-bounds).

Moreover, even in practice, the reachability problem is diﬃcult. Nowadays, no eﬃcient tool

exists for deciding it since the known algorithms are diﬃcult to be implemented and require

many enumerations in extremely large state spaces (see [6] for the state-of-the-art algorithm

deciding the general reachability problem).

Fortunately, easier natural variants of the reachability problem can be applied in various

contexts. For instance, the coverability problem, a variant of the reachability problem, can

be applied in the analysis of concurrent programs [1]. The coverability problem is known to

be exponential-space complete [20, 4], and eﬃcient tools exist [3, 9].

Another variant is the mutual reachability problem. This problem consists in deciding if

two conﬁgurations are mutually reachable one from the other. This problem was proved to

be exponential-space complete in [13] and ﬁnds unexpected applications in population pro-

tocols [7], trace logics [16], universality problems related to structural liveness problems [12],

and in solving the home state problem [2]. The exponential-space complexity upper-bound

2 Petri Net Mutual Reachability Relations

of the mutual reachability problem proved in [13] is obtained by observing that if two con-

ﬁgurations are mutually reachable, then the two conﬁgurations belong to a cycle of the

(inﬁnite) reachability graph with a length at most doubly-exponential with respect to the

size in binary of the two conﬁgurations.

Recently, the computation of a Presburger formula encoding the mutual reachability

problem found an application in the reachability problem of Petri nets extended with a

stack in [8]. In that paper, authors provided a formula of tower size and left open the

computation of a formula of elementary size.

Contribution. In this paper, we focus on the minimal size of a quantiﬁer-free Presburger

formula encoding the mutual reachability relation. We provide a way to compile the mutual

reachability relation of a Petri net with dcounters into a quantiﬁer-free Presburger formula

given as a doubly exponential disjunction of O(d) linear constraints of exponential size.

Outline. In Part I we provide algorithms for encoding in the quantiﬁer-free fragment

of the Presburger arithmetic the membership of vectors in lattices (see Section 2), and the

reachability relations of words of Petri net actions (see Section 3). In Part II we provide an

overview of the way quantiﬁer-free Presburger formula encoding the mutual reachability are

obtained. Results of that part are self-contains except two technical results that are proved

respectively in Part III and Part IV. In Part V we conclude the paper with an open problem

about the conﬁgurations of a Petri net in the bottom strongly-connected components of the

reachability graph.

Part I

Compiling in Presburger

In this part, we provide algorithms for encoding in the quantiﬁer-free fragment of the Pres-

burger arithmetic lattices (see Section 2) and reachability relations of words of Petri net

actions (see Section 3).

The set of rationals, integers, non-negative rationals, and natural numbers are denoted as

Q,Z,Q≥0, and Nrespectively. We denote by Xdthe set of d-dimensional vectors of elements

in X. Vectors are denoted in bold face, and given x∈Qd, we denote by x(1),...,x(d) its

components in such a way x= (x(1),...,x(d)). We denote by kxkthe one-norm Pd

i=1 |x(i)|,

and by kxk∞the inﬁnite-norm max1≤i≤d|x(i)|. Given two vectors x,y∈Qd, we denote by

x·ythe number Pd

i=1 x(i)y(i).

2 Lattices

Alattice is a subgroup of (Zd,+), i.e. a set L⊆Zdthat contains the zero vector 0, such

that x+y∈Lfor every x,y∈L, and such that −x∈Lfor every x∈L. The lattice

spanned by a ﬁnite sequence v1,...,vkof vectors in Zdis the lattice Zv1+···+Zvk. Let

us recall that any lattice is spanned by such a ﬁnite sequence. It follows that for any lattice

L⊆Zd, there is a Presburger formula encoding the membership of a vector vin Lof the

form ∃z1,...,zkv=z1v1+··· +zkvk. In order to obtain a quantiﬁer-free Presburger

formula encoding L, we can perform a quantiﬁer elimination from such a formula but it is

diﬃcult to obtain interesting complexity bounds with such an approach. We follow another

approach based on the notion of representations.

Arepresentation γof a lattice L⊆Zdis a tuples γdef

= ((n1,a1),...,(nd,ad)) of dpairs

(ni,ai)∈N×Zdsuch that the following equality holds:

L=(x∈Zd|

i=1

ai·x∈niZ)

We denote by JγKthe lattice Land by kγk∞the value max{n1,ka1k∞, . . . , nd,kadk∞}.

In this section we prove the following Theorem 1 that shows that lattices spanned by

ﬁnite sequences of vectors admits a representation computable in polynomial time (assuming

numbers encoded in binary). Such a representation will help encoding lattice membership

with a formula in the quantiﬁer-free fragment of the Presburger arithmetic. All other results

and deﬁnitions are not used in the sequel.

◮Theorem 1. Let Lbe the lattice spanned by a sequence of vectors in {−m, . . . , m}dencoded

in binary for some m∈N. We can compute in polynomial time a representation γof Lsuch

that kγk∞≤(d!)2md.

The proof is based on classical matrix operations over the rationals. We do not recall

classical notations and deﬁnitions we are using but brieﬂy recall some others.

Let Mbe a r×rsquare matrix. Let us recall that the determinant of M, denoted

as det(M) is deﬁned as Pσ∈Srsgn(σ)Qr

i=1 Miσ(i)where Sris the set of permutations of

{1,...,r}, and sgn(σ)∈ {−1,1}is the sign of σ. In particular if Mis an integer matrix

with coeﬃcients bounded by some m∈N, then det(M) is an integer bounded in absolute

value by r!mr. A r×rsquare matrix is said to be non-singular if det(M) is nonzero. Notice

that in this case there exists a unique r×rmatrix M−1such that M−1M=M M−1=Ir

where Iris the identity r×rsquare matrix, i.e. the matrix with zero coeﬃcients except on

the main diagonal where coeﬃcients are one. This matrix can be computed by introducing

the comatrice. Let us recall that the comatrix of any r×rsquare matrix Mis the r×r

square rational matrix com(M) satisfying (com(M))ij is det(Mij ) where Mij is the matrix

obtained from Mby replacing the jth column by a column of zeros, except on the ith line in

which we put a one. Let us recall that M⊤com(M) = det(M)Irwhere M⊤is the transpose

of M. It follows that if Mis non-singular then M−1=1

det(M)com(M)⊤. Notice that if the

coeﬃcients of Mare integers bounded in absolute value by some m∈N, then the coeﬃcients

of com(M) are integers bounded in absolute value by (r−1)!mr−1.

Let Mbe a r×kmatrix. The rank of Mis the maximal n∈ {0,...,min{r, k}} such

that Madmits a n×nnon-singular sub-matrix. Such a matrix Mis said to be full row

rank if its rank is equal to r. We say that such a matrix Mhas an Hermite normal form if

there exists a uni-modular matrix U(i.e. a matrix of integers with a +1 or −1 determinant)

such that M U = [H0] where His a non-singular, lower triangular, non-negative matrix, in

which each row has a unique maximum entry, which is located on the main diagonal of H.

Let us recall that every full row rank matrix Mhas a unique Hermite normal form [H0]

and moreover the uni-modular matrix Usuch that M U = [H0] is unique [21, Corollary

4.3b]. Additionally, if Mis an integral matrix then His a matrix of natural numbers.

Let us recall from [21, Section 10] that from a complexity point of view, the matrices U

and Hare computable in polynomial time and moreover det(H) divides the determinant of

any r×rnon-singular square sub-matrix of M. In particular, if the coeﬃcients of Mare

integers bounded in absolute value by some m∈N, then det(H), which is the product of

the diagonal elements of His bounded by r!mr. Let us recall that (com(H))ax = det(Hij )

where Hij is the matrix obtained from Mby replacing the jth column by a column of

zeros, except on the ith line in which we put a one. Now, let σbe a permutation of

{1,...,r}and observe that (Hij )kσ(k)≤Hkk for every k∈ {1, . . . , r}. It follows that

k=1(Hij )kσ(k)≤Qr

k=1 Hkk =δ(H). Therefore the coeﬃcients of com(H) are integers

bounded in absolute value by r! det(H)≤(r!)2mr.

Now, let us prove Theorem 1. We consider a lattice Lspanned by a sequence v1,...,vk

of vectors in {−m, . . . , m}d. We introduce the d×kmatrix Lobtained from this sequence

by considering vjas the jth column of L, i.e. Li,j =vj(i) for every 1 ≤i≤dand

1≤j≤k. We denote by rthe rank of L. Recall that r≤min{d, k}. By reordering columns

of L(which corresponds to a permutation of v1,...,vk) and by reordering the lines of L,

(which corresponds to a permutation of the components of L) we can assume without loss

of generality that Mcan be decomposed as follows where Ais a r×rnon-singular matrix,

Bis a (d−r)×rmatrix, A′is a r×(k−r) matrix, and B′is a (d−r)×(k−r) matrix.

L=A A′

B B′

Let us introduce the r×kmatrix Mdef

= [AA′]. Notice that Mis full row rank. It follows

that there exists a uni-modular matrix Usuch that M U is in Hermite normal form [H0].

We are ready for proving the following lemma.

◮Lemma 2. The lattice Lis the set of vectors x∈Zdsuch that:

(i) det(H)divides the coeﬃcients of [x(1) ...x(r)] com(H), and

(ii) det(A)[x(r+ 1) ...x(d)] = [x(1) ...x(r)] com(A)B⊤.

Proof. Since the rank of Lis equal to the rank of A, it follows that every line of [BB′] is

a linear combination of the lines of [AA′]. It follows that there exists a (d−r)×rrational

matrix Csuch that [BB′] = C[AA′]. Notice that this matrix Csatisﬁes C=BA−1since A

is non-singular.

Assume ﬁrst that x∈L.

Since xis a linear combination of the column vectors of L, and since the d−rlast

lines of Mare linear combinations of the lines of L, we deduce that xis also a linear

combination of the column vectors of M. Hence, there exists a sequence q1,...,qk∈Qsuch

that x=Pk

j=1 qjvj. From a matrix point of view, we have 





x(1)

x(d)





=M









. Since

M=A

CA , we deduce that xsatisﬁes (ii) by observing that det(A)A−1= com(T)⊤.

Next, observe that since x∈Lthen x=Pk

j=1 zjvjwith z1,...,zk∈Z. It follows that

we have:







x(1)

x(r)





=M









= [H0]U−1









=H





z′







Where z′

1,...,z′

kis the following sequence:







z′





=U−1











We have proved that xsatisﬁes (i).

Finally, assume that xis any vector in Zdsatisfying (i) and (ii). From (i), we deduce

that there exists z′

1,...,z′

r∈Zsuch that:

H−1





x(1)

x(r)





=





z′







We introduce the sequence z1,...,zkdeﬁned as follows where z′

r+1,...,z′

kare deﬁned as

zero:













def

=U





z′







Notice that we have:







x(1)

x(r)





= [H0]U−1









= [AA′]











文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

arXiv:2210.09931v1[cs.LO]18Oct2022CompilingPetriNetMutualReachabilityinPresburgerJérômeLerouxUniv.Bordeaux,CNRS,BordeauxINP,LaBRI,UMR5800,F-33400Talence,Francejerome.leroux@labri.frAbstractPetrinetsareaclassicalmodelofconcurrencywidelyusedandstudiedinformalveriﬁcationwithmanyapplicationsinmodelingan...

展开>> 收起<<

Compiling Petri Net Mutual Reachability in Presburger.pdf

共25页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Compiling Petri Net Mutual Reachability in Presburger

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: