The Library

Nets with tokens which carry data

Tools

Lazic, Ranko, Newcomb, T., Ouaknine, Joel, Roscoe, A. W. (Andrew William) and Worrell, J.. (2008) Nets with tokens which carry data. Fundamenta Informaticae, Vol.88 (No.3). pp. 251-274. ISSN 0169-2968

Full text not available from this repository.
Official URL: http://fi.mimuw.edu.pl

Abstract

We study data nets, a generalisation of Petri nets in which tokens carry data from linearly-ordered infinite domains and in which whole-place operations such as resets and transfers are possible. Data nets subsume several known classes of infinite-state systems, including multiset rewriting systems and polymorphic systems with arrays. We show that coverability and termination are decidable for arbitrary data nets, and that boundedness is decidable for data nets in which whole-place operations are restricted to transfers. By providing an encoding of lossy channel systems into data nets without whole-place operations, we establish that coverability, termination and boundedness for the latter class have non-primitive recursive complexity. The main result of the paper is that, even for unordered data domains (i. e., with only the equality predicate), each of the three verification problems for data nets without whole-place operations has non-elementary complexity.

Item Type: Journal Article
Subjects: Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions: Faculty of Science > Computer Science
Library of Congress Subject Headings (LCSH): Petri nets, Computer programs -- Verification, Computational complexity
Journal or Publication Title: Fundamenta Informaticae
Publisher: IOS Press
ISSN: 0169-2968
Date: 2008
Volume: Vol.88
Number: No.3
Number of Pages: 24
Page Range: pp. 251-274
Status: Peer Reviewed
Publication Status: Published
Access rights to Published version: Restricted or Subscription Access
Version or Related Resource: 28th International Conference on Applications and Theory of Petri Nets, Siedlce, Poland, Jun 25-29, 2007.
Conference Paper Type: Paper
Type of Event: Conference
URI: http://wrap.warwick.ac.uk/id/eprint/28727

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item View Item