Abstract: We present a compositional algebra of Petri nets, inspired by string diagrams used in mathematics and physics, that allows all nets to be expressed as a composition of a small number of basic net components. We argue that the resulting language allows the capture of distribution within a Petri net, which can be used to improve performance of model checking.
Abstract: In many practice-relevant applications, storing all states of a probabilistic system in memory is infeasible, and model checking tools break down. However, it is often the case that one can compute the successors of any given state in an efficient way. This opens up the door to sampling based approaches, which search the state space of the system for lassos offending the linear temporal property of interest. Unfortunately, such techniques are in general unable to sample the lasso space in a uniform way, which not only leads to inefficient search, but also hampers drawing any conclusion, in case no offending lasso is found. In this talk I will show that if one can (over)estimate the number of lassos in the system, one can devise a search technique that very accurately approximates uniform lasso sampling, with minimal memory requirements.
Patrolling is one of the central problems in operational security. Formally, a patrolling problem is specified by a set U of vulnerable targets and a function d which to every target u assigns the time d(u) ∈ N needed to complete an intrusion at u. The goal is to design an optimal strategy for a defender who is moving from target to target and aims at detecting possible intrusions. The defender can detect an intrusion at u only by visiting u before the intrusion is completed. The goal of the attacker is to maximize the probability of a successful attack. We assume that the attacker is adversarial, i.e., he knows the strategy of the defender and can observe her moves. We assume that all targets are equally important and that each move from target to target takes one unit of time.
We show that the defender has an optimal strategy for every patrolling problem. We also show that an optimal defender's strategy may require both memory and randomization, and may (inevitably) employ irrational probabilities.