More Like this

1. An Inclusive Study of Petri Nets and Their Applications

   McDuffie, Jasmine; Chenou, Jules (June 2024, Norfolk State University College of Science, Engineering and Technology. Technical Report No.1.)

   The main purpose of this report is to provide information on Petri nets, including their, design, semantics, properties, and uses. The problem addressed is how to model and analyze systems that may be susceptible to unknown issues. By visualizing these issues, we can improve or modify the system. Petri nets are highly powerful tools that can solve several problems, including issues with workflow management, deadlock, data transmission in communication systems, manufacturing and production, software systems, and more. These things are widely used in different work fields such as engineering, project management, and computer science. It is important to solve these problems for maintaining system reliability, and optimal performance. Exploring all the uses and techniques of a Petri net, beginning with the basics and advancing to the more complex ideas, demonstrates just how effective they are. The results confirm that Petri nets are important for identifying systems that need improvement within their performance and components across multiple fields. 

   more » « less
2. Reachability Set Generation Using Hybrid Relation Compatible Saturation

   https://doi.org/10.1007/978-3-030-61739-4_3  

   Biswal, Shruti; Miner, Andrew S (July 2020, Lecture notes in computer science)

   null; null (Ed.)

   Generating the state space of any finite discrete-state system using symbolic algorithms like saturation requires the use of decision diagrams or compatible structures for encoding its reachability set and transition relations. For systems that can be formally expressed using ordinary Petri Nets(PN), implicit relations, a static alternative to decision diagram-based representation of transition relations, can significantly improve the performance of saturation. However, in practice, some systems require more general models, such as self-modifying Petri nets, which cannot currently utilize implicit relations and thus use decision diagrams that are repeatedly rebuilt to accommodate the changing bounds of the system variables, potentially leading to overhead in saturation algorithm. This work introduces a hybrid representation for transition relations, that combines decision diagrams and implicit relations, to reduce the rebuilding overheads of the saturation algorithm for a general class of models. Experiments on several benchmark models across different tools demonstrate the efficiency of this representation. 

   more » « less
3. A compositional account of motifs, mechanisms, and dynamics in biochemical regulatory networks

   https://doi.org/10.32408/compositionality-6-2  

   Aduddell, Rebekah; Fairbanks, James; Kumar, Amit; Ocal, Pablo S; Patterson, Evan; Shapiro, Brandon T (May 2024, Compositionality)

   Regulatory networks depict promoting or inhibiting interactions between molecules in a biochemical system. We introduce a category-theoretic formalism for regulatory networks, using signed graphs to model the networks and signed functors to describe occurrences of one network in another, especially occurrences of network motifs. With this foundation, we establish functorial mappings between regulatory networks and other mathematical models in biochemistry. We construct a functor from reaction networks, modeled as Petri nets with signed links, to regulatory networks, enabling us to precisely define when a reaction network could be a physical mechanism underlying a regulatory network. Turning to quantitative models, we associate a regulatory network with a Lotka-Volterra system of differential equations, defining a functor from the category of signed graphs to a category of parameterized dynamical systems. We extend this result from closed to open systems, demonstrating that Lotka-Volterra dynamics respects not only inclusions and collapsings of regulatory networks, but also the process of building up complex regulatory networks by gluing together simpler pieces. Formally, we use the theory of structured cospans to produce a lax double functor from the double category of open signed graphs to that of open parameterized dynamical systems. Throughout the paper, we ground the categorical formalism in examples inspired by systems biology. 

   more » « less
4. Computing under-approximations of multivalued decision diagrams

   Hosseini, Seyedehzahra; Ciardo, Gianfranco (May 2023, Application and Theory of Petri Nets and Concurrency)

   Gomes, L.; Lorenz, R. (Ed.)

   Efficient manipulation of binary or multi-valueddecision diagrams (BDDs or MDDs) is critical in symbolic verification tools. Despite the applicability of MDDs to real-world tasks such as discovering the reachable states of a model, their large demands on hardware resources, especially memory, limit algorithmic scalability. In this paper, we focus on memory-constrained algorithms that employ a novel O(m log n)-time under-approximation technique for MDDs, where m and n are the number of MDD edges and nodes, respectively. The effectiveness of our approach is demonstrated experimentally by a reduction in peak memory usage for the symbolic reachability computation of a set of Petri nets. 

   more » « less
5. SOUPS: A Variable Ordering Metric for the Saturation Algorithm

   https://doi.org/10.1109/ACSD.2018.000-4  

   Smith, Benjamin; Ciardo, Gianfranco (June 2018, 2018 18th International Conference on Application of Concurrency to System Design (ACSD) (2018))

   Multivalued decision diagrams are an excellent technique to study the behavior of discrete-state systems such as Petri nets, but their variable order (mapping places to MDD levels) greatly affects efficiency, and finding an optimal order even just to encode a given set is NP-hard. In state-space generation, the situation is even worse, since the set of markings to be encoded keeps evolving and is known only at the end. Previous heuristics to improve the efficiency of the saturation algorithm often used in state-space generation seek a variable order minimizing a simple function of the Petri net, such as the sum over each transition of the top variable position (SOT) or variable span (SOS). This, too, is NP-hard, so we cannot compute orders that minimize SOT or SOS in most cases but, even if we could, it would have limited effectiveness. For example, SOT and SOS can be led astray by multiple copies of a transition (giving more weight to it), or transitions with equal inputs and outputs (giving weight to transitions that should be ignored). These anomalies inspired us to define SOUPS, a new heuristic that only takes into account the \emph{unique} and \emph{productive} portion of each transition. The SOUPS metric can be easily computed, allowing us to use it in standard search techniques like simulated annealing to find good orders. Experiments show that SOUPS is a much better proxy for the quantities we really hope to improve, the memory and time for MDD manipulation during state-space generation. 

   more » « less