Related papers: Accelerating the Computation of Dead and Concurren…

We propose a new method that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. Our approach relies on a state space abstraction, called polyhedral abstraction, which involves a…

Concurrent programming is used in all large and complex computer systems. However, concurrency errors and system failures (ex: crashes and deadlocks) are common. We find that Petri nets can be used to model concurrent systems and find and…

We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer…

Concurrency is an important aspect of Petri nets to describe and simulate the behavior of complex systems. Knowing which places and transitions could be executed in parallel helps to understand nets and enables analysis techniques and the…

We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an updated reachability…

Being able to find small Petri nets with the same behaviour as formal specifications of concurrent systems benefits both effective verification and practical implementation of such systems. This paper considers specifications given in the…

State-space reduction techniques, used primarily in model-checkers, all rely on the idea that some actions are independent, hence could be taken in any (respective) order while put in parallel, without changing the semantics. It is thus not…

Automatic analysis of highly crowded people has attracted extensive attention from computer vision research. Previous approaches for crowd counting have already achieved promising performance across various benchmarks. However, to deal with…

Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to resolve decisions by drawing from some probability distribution. Here we…

This paper introduces negotiations, a model of concurrency close to Petri nets, with multi-party negotiations as concurrency primitive. We study two fundamental analysis problems. The soundness problem consists in deciding if it is always…

We propose a method to count the number of reachable markings of a Petri net without having to enumerate these rst. The method relies on a structural reduction system that reduces the number of places and transitions of the net in such a…

Rule-based systems must solve complex matching problems within tight time constraints to be effective in real-time applications, such as planning and reactive control for AI agents, as well as low-latency relational database querying.…

We introduce a new method for speeding up the inference of deep neural networks. It is somewhat inspired by the reduced-order modeling techniques for dynamical systems.The cornerstone of the proposed method is the maximum volume algorithm.…

Low-overhead visual place recognition (VPR) is a highly active research topic. Mobile robotics applications often operate under low-end hardware, and even more hardware capable systems can still benefit from freeing up onboard system…

Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows how to solve model-checking problems using a combination of…

A wide variety of models for concurrent programs has been proposed during the past decades, each one focusing on various aspects of computations: trace equivalence, causality between events, conflicts and schedules due to resource accesses,…

Many engineering processes can be accurately modelled using partial differential equations (PDEs), but high dimensionality and non-convexity of the resulting systems pose limitations on their efficient optimisation. In this work, a model…

Petri net unfoldings are a useful tool to tackle state-space explosion in verification and related tasks. Moreover, their structure allows to access directly the relations of causal precedence, concurrency, and conflict between events.…

The theory of Petri Nets provides a general framework to specify the behaviors of real-time reactive systems and Time Petri Nets were introduced to take also temporal specifications into account. We present in this paper a forward…

We introduce polynomial couplings, a generalization of probabilistic couplings, to develop an algorithm for the computation of equivalence relations which can be interpreted as a lifting of probabilistic bisimulation to polynomial…