skip to main content

This content will become publicly available on October 25, 2024

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):
2026478 1925043
Author(s) / Creator(s):
; ; ; ;
Publisher / Repository:
Date Published:
Journal Name:
AAAI 2023 Fall Symposium Series
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. 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
  2. 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
  3. 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
  4. 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
  5. 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