skip to main content


This content will become publicly available on January 22, 2025

Title: Petri Nets for the Iterative Development of Interactive Robotic Systems
We argue for the use of Petri nets as a modeling language for the iterative development process of interactive robotic systems. Petri nets, particularly Timed Colored Petri nets (TCPNs), have the potential to unify various phases of the development process-design, specification, simulation, validation, implementation, and deployment. We additionally discuss future directions for creating a domain-specific variant of TCPNs tailored specifically for HRI systems development.  more » « less
Award ID(s):
1925043 2026478
NSF-PAR ID:
10505257
Author(s) / Creator(s):
; ; ; ;
Publisher / Repository:
AAAI
Date Published:
Journal Name:
Proceedings of the AAAI Symposium Series
Volume:
2
Issue:
1
ISSN:
2994-4317
Page Range / eLocation ID:
526 to 531
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. 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
  2. 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. Summary

    Cloud computing has attracted much attention recently in both industry field and academic research area. More and more Internet applications are moving to the cloud environment. However, it is difficult to construct perfectly secure mechanisms facing up with complex and various attacks in cloud computing, the efficient attack‐defense strategy is highly demanded. In this paper, a stochastic game model is proposed based on combining stochastic Petri nets with game theory, which is used to describe the attack‐defense behaviors in cloud computing. The physical machine, attack‐defense behavior, and their attributes are also modeled by stochastic game model thus forming the attack‐defense game model of cloud computing. On this basis, the Nash equilibrium of attack‐defense process in physical machine is computed to get the optimal defense strategy. The related theories of Petri nets and the reachable states of attack‐defense game model are used to formally verify the correctness and effectiveness of the proposed method. The enforcement algorithm is proposed to make cloud computing dynamically evaluate and select the defense strategy to against attack behavior as quickly as possible. Both case study and simulation results show that the proposed method can adapt quickly to the changes in cloud application thus improving the security of cloud computing.

     
    more » « less
  4. 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
  5. Decision diagrams are a well-established data structure for reachability set generation and model checking of high-level models such as Petri nets, due to their versatility and the availability of efficient algorithms for their construction. Using a decision diagram to represent the transition relation of each event of the high-level model, the saturation algorithm can be used to construct a decision diagram representing all states reachable from an initial set of states, via the occurrence of zero or more events. A difficulty arises in practice for models whose state variable bounds are unknown, as the transition relations cannot be constructed before the bounds are known. Previously, on-the-fly approaches have constructed the transition relations along with the reachability set during the saturation procedure. This can affect performance, as the transition relation decision diagrams must be rebuilt, and compute-table entries may need to be discarded, as the size of each state variable increases. In this paper, we introduce a different approach based on an implicit and unchanging representation for the transition relations, thereby avoiding the need to reconstruct the transition relations and discard compute-table entries. We modify the saturation algorithm to use this new representation, and demonstrate its effectiveness with experiments on several benchmark models. 
    more » « less