A well-structured framework for analysing petri net extensions

作     者：Finkel, A McKenzie, P Picaronny, C 

作者机构：Ecole Normale Super CNRS URA 8643 Lab Specificat & Verificat F-94235 Cachan France Univ Montreal Montreal PQ H3C 3J7 Canada 

出 版 物：《INFORMATION AND COMPUTATION》 (信息与计算)

年 卷 期：2004年第195卷第1-2期

页      面：1-29页

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 08[工学] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Foundation for Community Association Research, FCAR Natural Sciences and Engineering Research Council of Canada, NSERC Deutsche Forschungsgemeinschaft, DFG 

主　　题：lopic and verification of computer program theory of parallel and distributed computation algorithms decidability 

摘      要：Transition systems defined from recursive functions N-P -- N-P are introduced and named WSNs. or well-structured nets. Such nets sit conveniently between Petri net extensions and general transition systems. In the first part of this paper, we study decidability properties of WSN classes obtained by imposing natural restrictions on their defining functions, with respect to termination, coverability. and four variants of the boundedness problem. We are able to precisely answer almost all the questions which arise. thus gaining much insight into old and new generalized Petri net decidability results. In the second part. we specialize our analysis to WSNs defined from affine functions, which elegantly encompass most Petri net extensions studied in the literature. Again, we study decidability properties of natural classes of affine WSN with respect to the above six computational problems. In particular, we develop an algorithm computing limits of iterated nonnegative affine functions, in order to decide the path-place variant of the boundedness problem for non-negative affine WSN. (C) 2004 Published by Elsevier Inc.