# Tuesday, 28 February 2017: NODES Seminar, Newcastle

General meeting of all members of NODES and their PhD students.

## Location:

Room TR4, 4th Floor, Herschel Building, Newcastle University

## Timetable:

14.00-14.45 Andrew Wade (Durham, Maths): Convex hulls of random walks

14.45-15.30 Tea/Coffee break

15.30-16.15 Victor Khomenko (Newcastle, CS): Canonical Prefixes of Petri Net Unfoldings

Andrew Wade (Durham, Maths): Convex hulls of random walks

Abstract: On each of n unsteady steps, a drunken gardener drops a seed. Once the flowers have bloomed, what is the minimum length of fencing required to enclose the garden? What is its area? I will describe recent work on the convex hull of planar random walk, concerned in particular with the large-n asymptotics of its perimeter length and area. We provide variance asymptotics and distributional limit theorems. Of the four combinations of the two quantities (perimeter and area) in the two regimes (zero drift or non-zero drift for the steps of the walk), one limit is Gaussian; three are not.

This talk is mostly based on joint work with Chang Xu (Strathclyde); I’ll also mention ongoing work with Ostap Hryniv and James McRedmond (Durham).

Victor Khomenko (Newcastle, CS): Canonical Prefixes of Petri Net Unfoldings

Petri net unfolding prefixes are used for efficient formal verification of concurrent systems. For this, they have to be finite and complete, i.e. preserve the sufficient information about the original system to be able to decide whether a particular property holds. A key aspect is how to truncate the full (usually infinite) unfolding in such a way that the resulting prefix is guaranteed to be finite and complete. We present a new theoretical framework that allows one to define the unique canonical prefix of the unfolding. Canonical prefixes are complete in the new, stronger sense, and we provide necessary and sufficient conditions for its finiteness, as well as upper bounds on its size in certain cases. A surprising result is that the existing unfolding algorithms, despite being non-deterministic, always generate this canonical prefix.

Snapshots of the talks