Lean Reachability Tree for Unbounded Petri Nets

2018 ◽  
Vol 48 (2) ◽  
pp. 299-308 ◽  
Author(s):  
Jun Li ◽  
Xiaolong Yu ◽  
MengChu Zhou ◽  
Xianzhong Dai
Keyword(s):  
Petri Nets ◽  
Reachability Tree

ALGORITHM FOR CONSTRUCTING A REACHABILITY TREE FOR STOCHASTIC PETRI NETS

2021 ◽  
pp. 34-40
Author(s):  
Д.С. Звягин
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Final Stage ◽  
Distribution Systems ◽  
Stochastic Petri Nets ◽  
Matrix Equations ◽  
Correct Process ◽  
Reachability Sets ◽  
Process Failures ◽  
Reachability Tree

Описываются основные определения дерева достижимости сетей Петри. Также рассматриваются различные примеры стохастических сетей Петри, в которых после выставления начальных маркировок в первых позициях определяются значения во всех остальных позициях. Показаны примеры определения маркировок при помощи высчитывания вектора диагональной свертки. Для каждого примера стохастической сети Петри проводится анализ данной сети. Данный анализ необходим для различных распределительных систем и процессов, особенно на заключительном этапе. Основными методами анализа являются дерево достижимости и матричные уравнения. Рассматривается один из таких методов анализа сетей Петри. С использованием дерева достижимости можно проанализировать, выявить и исправить сбои в процессах, которые могут произойти при наличии тупиковых состояний и при неправильной последовательности срабатывания переходов. Исходя из рассмотренных примеров предлагается обобщенный алгоритм построения дерева достижимости для стохастических сетей Петри. Предложенный алгоритм построения дерева достижимости стохастических сетей Петри можно применять для всех сетей как с конечным, так и с бесконечным множеством достижимости. Данный алгоритм будет являться полезным инструментом при анализе стохастических сетей Петри The article describes the basic definitions of the reachability tree of Petri nets. It also considers various examples of stochastic Petri nets, in which, after setting the initial markings in the first positions, the values in all other positions are determined. The work shows examples of determining markings by calculating the vector of the diagonal convolution. Each example of a stochastic Petri net is analyzed. This analysis is necessary for various distribution systems and processes, especially in the final stage. The main analysis methods are reachability tree and matrix equations. I consider one of such methods for analyzing Petri nets. Using the reachability tree, you can analyze, identify, and correct process failures that can occur when there are deadlocks and when transitions are fired incorrectly. Based on the examples considered, I propose a generalized algorithm for constructing a reachability tree for stochastic Petri nets. The proposed algorithm for constructing the reachability tree of stochastic Petri nets can be applied to all nets with both finite and infinite reachability sets. This algorithm will be a useful tool for analyzing stochastic Petri nets

Using Time Reachability Tree Logic to Specifying and Verifying Temporal Behavior of Workflow-Net

2014 ◽  
Vol 571-572 ◽  
pp. 528-534
Author(s):  
Chyun Chyi Chen ◽  
Yueh Min Huang
Keyword(s):  
Petri Nets ◽  
Workflow Management ◽  
Schedulability Analysis ◽  
Temporal Behavior ◽  
Time Petri Nets ◽  
Reachability Graph ◽  
Workflow Execution ◽  
Workflow System ◽  
Timing Properties ◽  
Reachability Tree

Workflow management has been a hot issue in both academic and industrial research. Deadline assignment is of great significance in workflow management. In order to avoid deadline violation, this paper presents an approach to the schedulability analysis of workflow system modeled in p-time Petri nets by separating timing properties from other behavior properties. The analysis of behavioral properties is conducted based on the reachability graph of the underlying p-Time Petri net, whereas timing constraints are checked in term of absolute and relative firing domains. Our technique is based on a concept called clock-stamped state class (CS-class) and temporal logic. With the reachability graph generated based on CS-class, we can directly compute the end-to-end time delay in workflow execution. We have identified a class of well-structured p-time Petri nets such that their reachability can be easy analyzed and temporal behavior can be easy analyzed by time reachability tree logical.

scholarly journals Modeling a New AQM Model for Internet Chaotic Behavior Using Petri Nets

2021 ◽  
Vol 11 (13) ◽  
pp. 5877
Author(s):  
José M. Amigó ◽  
Guillem Duran ◽  
Ángel Giménez ◽  
José Valero ◽  
Oscar Martinez Bonastre
Keyword(s):  
Petri Nets ◽  
Queue Length ◽  
Chaotic Behavior ◽  
Stability Control ◽  
Formal Modeling ◽  
Random Early Detection ◽  
Network Algorithms ◽  
The Matrix ◽  
Invariant Analysis ◽  
Reachability Tree

Formal modeling is considered one of the fundamental phases in the design of network algorithms, including Active Queue Management (AQM) schemes. This article focuses on modeling with Petri nets (PNs) a new scheme of AQM. This innovative AQM is based on a discrete dynamical model of random early detection (RED) for controlling bifurcations and chaos in Internet congestion control. It incorporates new parameters (α,β) that make possible better stability control over oscillations of an average queue length (AQL) at the router. The PN is validated through the matrix equation approach, reachability tree, and invariant analysis. The correctness is validated through the key properties of reachability, boundedness, reversibility, deadlock, and liveness.

scholarly journals Existence of Forbidden Digraphs for Crisp Boolean Petri Nets

2019 ◽  
Vol 5 (1) ◽  
pp. 83-95
Author(s):  
Gajendra Pratap Singh ◽  
Sujit Kumar Singh ◽  
Madhuri Jha
Keyword(s):  
Mathematical Modeling ◽  
Petri Nets ◽  
Petri Net ◽  
Execution Time ◽  
Graph Model ◽  
Minimum Number ◽  
Reachability Tree

Boolean Petri net (BPN) and Crisp Boolean Petri net (CBPN) is a well-studied graph model since 2010 which has several applications in mathematical modeling of complex or tricky networks. Modeling any network with Petri net which can generate binary numbers as marking vectors in its reachability tree is still has much uses. In CBPN with a minimum number of transition and minimum number of steps of reachability tree, minimal execution time to run the machine has not been noted till date, thus it’s necessary to sort out this problem. Possibly it may occur due to some forbidden structure which hinders any 1-safe Petri net to be a CBPN. In this paper, we present some forbidden digraphs whose presence interrupts the generation of binary n-vectors exactly once. Any 1-safe Petri net is not a CBPN if it contains any of the subnet induced to the four forbidden structures discussed in this paper.

A New Modified Reachability Tree Approach and Its Applications to Unbounded Petri Nets

2013 ◽  
Vol 43 (4) ◽  
pp. 932-940 ◽  
Author(s):  
ShouGuang Wang ◽  
MengChu Zhou ◽  
ZhiWu Li ◽  
ChengYing Wang
Keyword(s):  
Petri Nets ◽  
Reachability Tree ◽  
Tree Approach

SPECIFYING AND VERIFYING TEMPORAL BEHAVIOR OF HIGH ASSURANCE SYSTEMS USING REACHABILITY TREE LOGIC

1999 ◽  
Vol 09 (02) ◽  
pp. 233-249
Author(s):  
STEPHEN J. H. YANG ◽  
WILLIAM CHU ◽  
JONATHAN LEE
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Petri Net ◽  
System Modeling ◽  
Model System ◽  
Temporal Behavior ◽  
Time Petri Net ◽  
High Assurance ◽  
System Requirements ◽  
Reachability Tree

This paper presents our reachability tree logic (RTL) and its integration with time Petri nets to specify and verify the temporal behavior of high assurance systems. The specification phase begins with a system modeling to model system requirements into a time Petri net N and construct a reachability tree RT of N. We then use RTL to specify the desired temporal behavior as formula F. The verification phase uses a model-checking algorithm to check whether RT can satisfy F, that is to find firing sequences to satisfy F. If F is not satisfied, we then modify N into N′ and obtain a RT′ of the modified N′. The modification (refinement) continues until the modified RT′ can satisfy F. In addition, we will demonstrate how to reduce the complexity of model-checking by using our RTL-based algorithm. We have implemented a specification and verification toolkit called NCUPN (National Central University Petri Nets toolkit) using Java. NCUPN is now available on the Internet via

Sign in / Sign up

Export Citation Format

Share Document