We study timed Petri nets, with preselection and priority routing. We
represent the behavior of these systems by piecewise affine dynamical systems.
We use tools from the theory of nonexpansive mappings to analyze these systems.
We establishan equivalence theorem between priority-free fluid timed Petri nets
and semi-Markov decision processes, from which we derive the convergence to a
periodic regime and the polynomial-time computability of the throughput. More
generally, we develop an approach inspired by tropical geometry, characterizing
the congestion phases as the cells of a polyhedral complex. We illustrate these
results by a current application to the performance evaluation of emergency
call centers in the Paris area. We show that priorities can lead to a
paradoxical behavior: in certain regimes, the throughput of the most prioritary
task may not be an increasing function of the resources.
To identify the causes of performance problems or to predict process
behavior, it is essential to have correct and complete event data. This is
particularly important for distributed systems with shared resources, e.g., one
case can block another case competing for the same machine, leading to
inter-case dependencies in performance. However, due to a variety of reasons,
real-life systems often record only a subset of all events taking place. To
understand and analyze the behavior and performance of processes with shared
resources, we aim to reconstruct bounds for timestamps of events in a case that
must have happened but were not recorded by inference over events in other
cases in the system. We formulate and solve the problem by systematically
introducing multi-entity concepts in event logs and process models. We
introduce a partial-order based model of a multi-entity event log and a
corresponding compositional model for multi-entity processes. We define
PQR-systems as a special class of multi-entity processes with shared resources
and queues. We then study the problem of inferring from an incomplete event log
unobserved events and their timestamps that are globally consistent with a
PQR-system. We solve the problem by reconstructing unobserved traces of
resources and queues according to the PQR-model and derive bounds for their
timestamps using a linear program. While the problem is illustrated for
material handling systems like baggage handling systems in airports, […]
We prove that $\omega$-languages of (non-deterministic) Petri nets and
$\omega$-languages of (non-deterministic) Turing machines have the same
topological complexity: the Borel and Wadge hierarchies of the class of
$\omega$-languages of (non-deterministic) Petri nets are equal to the Borel and
Wadge hierarchies of the class of $\omega$-languages of (non-deterministic)
Turing machines. We also show that it is highly undecidable to determine the
topological complexity of a Petri net $\omega$-language. Moreover, we infer
from the proofs of the above results that the equivalence and the inclusion
problems for $\omega$-languages of Petri nets are $\Pi_2^1$-complete, hence
also highly undecidable.
Additionally, we show that the situation is quite the opposite when
considering unambiguous Petri nets, which have the semantic property that at
most one accepting run exists on every input. We provide a procedure of
determinising them into deterministic Muller counter machines with counter
copying. As a consequence, we entail that the $\omega$-languages recognisable
by unambiguous Petri nets are $\Delta^0_3$ sets.
State-of-the-art process discovery methods construct free-choice process
models from event logs. Consequently, the constructed models do not take into
account indirect dependencies between events. Whenever the input behaviour is
not free-choice, these methods fail to provide a precise model. In this paper,
we propose a novel approach for enhancing free-choice process models by adding
non-free-choice constructs discovered a-posteriori via region-based techniques.
This allows us to benefit from the performance of existing process discovery
methods and the accuracy of the employed fundamental synthesis techniques. We
prove that the proposed approach preserves fitness with respect to the event
log while improving the precision when indirect dependencies exist. The
approach has been implemented and tested on both synthetic and real-life
datasets. The results show its effectiveness in repairing models discovered
from event logs.
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 techniques that stay in complexity proportional to the size of
the net structure rather than to the state-space size.
We combine an SMT based over-approximation to prove that some behaviors are
unfeasible, an under-approximation using memory-less sampling of runs to find
witness traces or counter-examples, and a set of structural reduction rules
that can simplify both the system and the property.
This approach was able to win by a clear margin the model-checking contest
2020 for reachability queries as well as deadlock detection, thus demonstrating
the practical effectiveness and general applicability of the system of rules
presented in this paper.