The first part of the paper is an introduction to the theory of probabilistic
concurrent systems under a partial order semantics. Key definitions and results
are given and illustrated on examples. The second part includes contributions.
We introduce deterministic concurrent systems as a subclass of concurrent
systems. Deterministic concurrent system are "locally commutative'" concurrent
systems. We prove that irreducible and deterministic concurrent systems have a
unique probabilistic dynamics, and we characterize these systems by means of
their combinatorial properties.
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 property on a reduced version of this net. This method relies on a
new state space abstraction based on systems of constraints, called polyhedral
abstraction. We prove the correctness of this method using a new notion of
equivalence between nets. We provide a complete framework to define and check
the correctness of equivalence judgements; prove that this relation is a
congruence; and give examples of basic equivalence relations that derive from
structural reductions. Our approach has been implemented in a tool, named SMPT,
that provides two main procedures: Bounded Model Checking (BMC) and Property
Directed Reachability (PDR). Each procedure has been adapted in order to use
reductions and to work with arbitrary Petri nets. We tested SMPT on a large
collection of queries used in the Model Checking Contest. Our experimental
results show that our approach works well, even when we only have a moderate
amount of reductions.
Petri net synthesis consists in deciding for a given transition system $A$
whether there exists a Petri net $N$ whose reachability graph is isomorphic to
$A$. Several works examined the synthesis of Petri net subclasses that
restrict, for every place $p$ of the net, the cardinality of its preset or of
its postset or both in advance by small natural numbers $\varrho$ and $\kappa$,
respectively, such as for example (weighted) marked graphs, (weighted)
T-systems and choice-free nets. In this paper, we study the synthesis aiming at
Petri nets which have such restricted place environments, from the viewpoint of
classical and parameterized complexity: We first show that, for any fixed
natural numbers $\varrho$ and $\kappa$, deciding whether for a given transition
system $A$ there is a Petri net $N$ such that (1) its reachability graph is
isomorphic to $A$ and (2) for every place $p$ of $N$ the preset of $p$ has at
most $\varrho$ and the postset of $p$ has at most $\kappa$ elements is doable
in polynomial time. Secondly, we introduce a modified version of the problem,
namely Environment Restricted Synthesis (ERS, for short), where $\varrho$ and
$\kappa$ are part of the input, and show that ERS is NP-complete, regardless
whether the sought net is impure or pure. In case of the impure nets, our
methods also imply that ERS parameterized by $\varrho+\kappa$ is $W[2]$-hard.
In Petri net synthesis we ask whether a given transition system $A$ can be
implemented by a Petri net $N$. Depending on the level of accuracy, there are
three ways how $N$ can implement $A$: an embedding, the least accurate
implementation, preserves only the diversity of states of $A$; a language
simulation already preserves exactly the language of $A$; a realization, the
most accurate implementation, realizes the behavior of $A$ exactly. However,
whatever the sought implementation, a corresponding net does not always exist.
In this case, it was suggested to modify the input behavior -- of course as
little as possible. Since transition systems consist of states, events and
edges, these components appear as a natural choice for modifications. In this
paper we show that the task of converting an unimplementable transition system
into an implementable one by removing as few states or events or edges as
possible is NP-complete -- regardless of what type of implementation we are
aiming for; we also show that the corresponding parameterized problems are
$W[2]$-hard, where the number of removed components is considered as the
parameter; finally, we show there is no $c$-approximation algorithm (with a
polynomial running time) for neither of these problems, for every constant
$c\geq 1$.
A fundamental advantage of Petri net models is the possibility to
automatically compute useful system invariants from the syntax of the net.
Classical techniques used for this are place invariants, P-components, siphons
or traps. Recently, Bozga et al. have presented a novel technique for the
\emph{parameterized} verification of safety properties of systems with a ring
or array architecture. They show that the statement \enquote{for every instance
of the parameterized Petri net, all markings satisfying the linear invariants
associated to all the P-components, siphons and traps of the instance are safe}
can be encoded in \acs{WS1S} and checked using tools like MONA. However, while
the technique certifies that this infinite set of linear invariants extracted
from P-components, siphons or traps are strong enough to prove safety, it does
not return an explanation of this fact understandable by humans. We present a
CEGAR loop that constructs a \emph{finite} set of \emph{parameterized}
P-components, siphons or traps, whose infinitely many instances are strong
enough to prove safety. For this we design parameterization procedures for
different architectures.
Uniform coloured Petri nets can be abstracted to their skeleton, the
place/transition net that simply turns the coloured tokens into black tokens. A
coloured net and its skeleton are related by a net morphism. For the
application of the skeleton as an abstraction method in the model checking
process, we need to establish a simulation relation between the state spaces of
the two nets. Then, universal temporal properties (properties of the $ ACTL^* $
logic) are preserved. The abstraction relation induced by a net morphism is not
necessarily a simulation relation, due to a subtle issue related to deadlocks.
We discuss several situations where the abstraction relation induced by a net
morphism is as well a simulation relation, thus preserving $ACTL^*$ properties.
We further propose a partition refinement algorithm for folding a
place/transition net into a coloured net. This way, skeleton abstraction
becomes available for models given as place/transition nets. Experiments
demonstrate the capabilities of the proposed technology. Using skeleton
abstraction, we are capable of solving problems that have not been solved
before in the Model Checking Contest.