Advances in Concurrent System Modeling and Analysis

The field of concurrent system modeling and analysis is witnessing significant developments, with a focus on enhancing the expressiveness and tractability of various formalisms. Researchers are exploring new paradigms, such as nets-within-nets and data nets, to capture complex behaviors and interactions. The study of verification problems, including reachability and coverability, remains a central theme, with notable progress in characterizing the complexity of these problems for various classes of systems. Furthermore, the investigation of symmetric and branching systems is yielding new insights into the decidability and complexity of key decision problems. Noteworthy papers include:

  • One paper establishes the decidability of the reachability problem for 2-dimensional Branching VASS, providing a semilinear presentation of the reachability set.
  • Another paper investigates the reachability problem in symmetric VASS, achieving a PSPACE solution for symmetric groups and exploring the complexity gain for combined groups.

Sources

Wait-Only Broadcast Protocols are Easier to Verify

Nets-within-Nets through the Lens of Data Nets

On the Reachability Problem for Two-Dimensional Branching VASS

Reachability in symmetric VASS

Built with on top of