Top

Innovations in Systems and Software Engineering

Published in:

04-02-2020 | S.I. : VeCoS 2018

Exploiting local persistency for reduced state-space generation

Authors: K. Barkaoui, H. Boucheneb, Z. Li

Published in: Innovations in Systems and Software Engineering | Issue 2/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

This paper deals with two partial order techniques for Petri nets (PN in short): persistent sets and step graphs. These techniques aim to reduce the width and the depth of the marking graphs of PN, respectively, while preserving their deadlocks. To achieve more reductions while preserving the deadlocks of PN, this paper revisits the definition of persistent sets and establishes some weaker practical sufficient conditions. It also proposes a combination of persistent sets with steps as a sort of Cartesian product of persistent sets. This combination provides a means of better controlling the length and the number of steps, while still preserving deadlocks.

previous article LTL model checking for communicating concurrent programs

next article Timed service contract automata

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

http://projects.laas.fr/tina//home.php.

A strong/weak-persistent selective search from a marking M is a procedure that recursively computes a weak-persistent set and the successor markings reachable by each transition of this set, for M and each new computed marking [19].

The notation \(\mu _i \models D0 \wedge D1 \wedge D2\) means that \(\mu _i\) satisfies the conditions D0, D1 and D2.

http://mcc.lip6.fr.

There is a directed path between every two nodes (places or transitions) of the Petri net.

Abdulla PA, Aronis S, Jonsson B, Sagonas K (2017) Source sets: a foundation for optimal dynamic partial order reduction. J ACM 64(4):25:1–25:49CrossRefMathSciNet

Barkaoui K, Boucheneb H, Li Z (2018) Exploiting local persistency for reduced state space generation. In: International conference on verification and evaluation of computer and communication systems (VECoS), volume 11181 of Lecture Notes in Computer Science, pp 166–181

Barkaoui K, Couvreur J-M, Klai K (2005) On the equivalence between liveness and deadlock-freeness in Petri nets. In: Applications and theory of Petri nets 2005, 26th international conference, ICATPN 2005, Miami, USA, June 20–25, 2005, proceedings, pp 90–107

Barkaoui K, Pradat-Peyre J-F (1996) On liveness and controlled siphons in Petri nets. In: Application and theory of Petri nets 1996, 17th international conference, Osaka, Japan, June 24–28, 1996, proceedings, pp 57–72

Chen Y (2015) Optimal supervisory control of flexible manufacturing systems. Thesis. Le Cnam

Chen YF, Li ZW, Barkaoui K (2014) New Petri net structure and its application to optimal supervisory control: interval inhibitor arcs. IEEE Trans Syst Man Cybern 44(10):1384–1400CrossRef

Desel J, Juhás G (2001) ”What is a Petri net?”. In: Unifying Petri nets, advances in Petri Nets, pp 1–25

Godefroid P (1996) Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, volume 1032 of Lecture Notes in Computer Science. Springer

Iordache MV (2006) Deadlock and liveness properties of Petri nets. Birkhäuser, Boston, pp 125–151

10.

Junttila T (2005) On the symmetry reduction method for Petri nets and similar formalisms. In PhD dissertation, Helsinki University of Technology, Espoo, Finland

11.

Li ZW, Zhao M (2008) On controllability of dependent siphons for deadlock prevention in generalized Petri nets. IEEE Trans Syst Man Cybern 38(2):369–384CrossRef

12.

Peled D (1993) All from one, one for all: on model checking using representatives. In: Computer aided verification, 5th international conference, CAV ’93, Elounda, Greece, June 28–July 1, 1993, proceedings, pp 409–423

13.

Peled D, Wilke T (1997) Stutter-invariant temporal properties are expressible without the next-time operator. Inf Process Lett 63(5):243–246CrossRefMathSciNet

14.

Peterson JL (1981) Petri net theory and the modeling of systems. Prentice Hall PTR, Upper Saddle RiverMATH

15.

Ribet P-O, Vernadat F, Berthomieu B (2002) On combining the persistent sets method with the covering steps graph method. In: Formal techniques for networked and distributed systems—FORTE 2002, 22nd IFIP WG 6.1 International conference Houston, Texas, USA, Nov 11–14, 2002, proceedings, pp 344–359

16.

Valmari A (1992) A stubborn attack on state explosion. Formal Methods Syst Des 1(4):297–322CrossRef

17.

Valmari A (1996) The state explosion problem. In: Lectures on Petri nets I: basic models, advances in Petri nets, the volumes are based on the advanced course on Petri nets, held in Dagstuhl, Sept 1996, pp 429–528

18.

Valmari A, Hansen H (2011) Can stubborn sets be optimal? Fundam Inform 113(3–4):377–397CrossRefMathSciNet

19.

Valmari A, Hansen H (2017) Stubborn set intuition explained. Trans Petri Nets Other Models Concurr 12:140–165CrossRefMathSciNet

20.

van der Aalst W (1998) Finding errors in the design of a workflow process: a Petri-net-based approach. In: Workflow management: net-based concepts, models, techniques, and tools (WFM ’98): proceedings of the workshop, June 22, 1998, Lisbon, Portugal, Computing Science Reports. Technische Universiteit Eindhoven, pp 60–81

21.

Vernadat F, Azéma P, Michel F (1996) Covering step graph. In: Application and theory of Petri nets 1996, 17th international conference, Osaka, Japan, June 24–28, 1996, proceedings, pp 516–535

22.

Wildberger NJ (2003) A new look at multiset. In: School of Mathematics, UNSW Sydney 2052, pp 1–21

Title: Exploiting local persistency for reduced state-space generation
Authors: K. Barkaoui
H. Boucheneb
Z. Li
Publication date: 04-02-2020
Publisher: Springer London
Published in: Innovations in Systems and Software Engineering / Issue 2/2020
Print ISSN: 1614-5046
Electronic ISSN: 1614-5054
DOI: https://doi.org/10.1007/s11334-020-00358-3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2/2020

Combined software and hardware fault injection vulnerability detection

Preface to the VECoS 2018 special issue of ISSE

Stochastic modeling and analysis of road–tramway intersections

LTL model checking for communicating concurrent programs

Improving swarming using genetic algorithms

How to be sure a faulty system does not always appear healthy?

Premium Partner