Proving nonreachability by modulo-invariants

被引：9

作者：

Desel, J

Neuendorf, KP

Radola, MD

机构：

[1] HUMBOLDT UNIV BERLIN,INST INFORMAT,D-10099 BERLIN,GERMANY

[2] TECH UNIV MUNICH,INST INFORMAT,D-80290 MUNICH,GERMANY

来源：

THEORETICAL COMPUTER SCIENCE | 1996年 / 153卷 / 1-2期

关键词：

D O I：

10.1016/0304-3975(95)00117-4

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We introduce modulo-invariants of Petri nets which are closely related to classical place-invariants but operate in residue classes module k instead of natural or rational numbers. Whereas place-invariants prove the nonreachability of a marking if and only if the corresponding marking equation has no solution in Q, a marking can be proved nonreachable by modulo-invariants if and only if the marking equation has no solution in Z. We show how to derive from each net a finite set of invariants - containing place-invariants and modulo-invariants - such that if any invariant proves the nonreachability of a marking, then some invariant of this set proves that the marking is not reachable.

引用

下载

页码：49 / 64

页数：16

共 36 条

[21] Invariants of GLn(Fq) in polynomials modulo Frobenius powers
Lewis, J.
Reiner, V.
Stanton, D.
PROCEEDINGS OF THE ROYAL SOCIETY OF EDINBURGH SECTION A-MATHEMATICS, 2017, 147 (04) : 831 - 873
[22] ISOMORPHISM INVARIANTS FOR ABELIAN GROUPS MODULO BOUNDED GROUPS
ENSEY, RJ
PACIFIC JOURNAL OF MATHEMATICS, 1968, 24 (01) : 71 - &
[23] MOTIVIC SERRE INVARIANTS MODULO THE SQUARE OF L-1
Yasuda, Takehiko
PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY, 2018, 146 (02) : 547 - 554
[24] Property-Directed Inference of Universal Invariants or Proving Their Absence
Karbyshev, Aleksandr
Bjorner, Nikolaj
Itzhaky, Shachar
Rinetzky, Noam
Shoham, Sharon
JOURNAL OF THE ACM, 2017, 64 (01)
[25] Property-Directed Inference of Universal Invariants or Proving Their Absence
Karbyshev, A.
Bjorner, N.
Itzhaky, S.
Rinetzky, N.
Shoham, S.
COMPUTER AIDED VERIFICATION, PT I, 2015, 9206 : 583 - 602
[26] Generating modulo-2 linear invariants for hardware model checking
Aleksandrowicz, Gadi, 1600, Springer Verlag (8855):
[27] The invariants, seminvariants and linear covariants of binary quartic form modulo 2.
Dickson, LE
ANNALS OF MATHEMATICS, 1913, 15 : 114 - 117
[28] Infinitesimal invariants for cycles modulo algebraic equivalence and 1-cycles on Jacobians
Voisin, Claire
ALGEBRAIC GEOMETRY, 2014, 1 (02): : 140 - 165
[29] An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants
Liu, Jie
Liu, Jing
Zhang, Miaomiao
Sun, Haiying
Chen, Xiaohong
Du, Dehui
Chen, Mingsong
2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2017, : 138 - 143
[30] Automatic proving or disproving equality loop invariants based on finite difference techniques
Li, Mengjun
INFORMATION PROCESSING LETTERS, 2015, 115 (04) : 468 - 474

← 1 2 3 4 →