NDLI: Checking Partial-Order Properties of Vector Addition Systems with States

Content Provider	IEEE Xplore Digital Library
Author	Avellaneda, F. Morin, R.
Copyright Year	2013
Description	Author affiliation: Lab. d'Inf. Fondamentale de Marseille, Aix-Marseille Univ., Marseille, France (Avellaneda, F.; Morin, R.)
Abstract	Message Sequence Graphs (MSGs) form a popular model often used for the documentation of telecommunication protocols. They consist of typical scenarios of message exchanges depicted as partial-orders of events that lead from one control state to another. On the other hand Petri nets are a well-known formalism for distributed or parallel systems based on the notion of token game. Both approaches profit by a visual presentation and are the subject of numerous formal verification techniques and tools. In this paper we investigate a formalism which provides MSGs with the notion of token game and extends Petri nets with both control states and partial orders. Providing Petri nets with control states corresponds precisely to the model of Vector Addition Systems with States (VASSs). Thus we need to define first a partial-order semantics for VASSs which adopts the basic features of communication scenarios. To do so we extend simply the process semantics of Petri nets. We obtain a formal model that enjoys several interesting properties in terms of expressiveness and concision. The addition of control states to Petri nets under the partial-order semantics leads to undecidable problems. Similarly to MSGs, one cannot decide in particular whether two given VASSs describe the same process language. However we show that basic problems about the set of markings reached along the processes of a VASS, such as boundedness, covering and reachability, can be reduced to the analogous problems for Petri nets. This relies on a new technique that simulates all prefixes of all processes. In this way Petri net tools can be used to verify the properties of a VASS under the process semantics. We present also a technique to check effectively any MSO property of these partial orders, provided that the given system is bounded. This enables us to tackle more verification problems and subsumes known results for the model checking of MSGs. All algorithms presented in this paper have been implemented in a prototype tool available online.
Starting Page	100
Ending Page	109
File Size	439011
Page Count	10
File Format	PDF
ISBN	9780769550350
ISSN	15504808
DOI	10.1109/ACSD.2013.13
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2013-07-08
Publisher Place	Spain
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Petri nets Semantics Vectors Computational modeling Protocols Process control Labeling Monadic second-order logic Vector addition system with states Process semantics Reachability properties
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Vector addition systems with states vs. Petri nets (2012).

Vector Addition Systems with States vs. Petri Nets

Petri Net Reachability Graphs: Decidability Status of FO Properties

Vector Addition Systems with States vs. Petri Nets

Guidelines for the Verification of Population Protocols

On the Context-Freeness Problem for Vector Addition Systems

A Behavioral Analysis Approach for Efficient Partial Order Reduction

Context petri nets, vector addition systems (vas) and vector addition.

Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets (2002)

Checking Partial-Order Properties of Vector Addition Systems with States

Similar Documents

Vector addition systems with states vs. Petri nets (2012).

Vector Addition Systems with States vs. Petri Nets

Petri Net Reachability Graphs: Decidability Status of FO Properties

Vector Addition Systems with States vs. Petri Nets

Guidelines for the Verification of Population Protocols

On the Context-Freeness Problem for Vector Addition Systems

A Behavioral Analysis Approach for Efficient Partial Order Reduction

Context petri nets, vector addition systems (vas) and vector addition.

Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets (2002)

Checking Partial-Order Properties of Vector Addition Systems with States