Nominal Sets meet Automata Theory
Warsaw, Poland, 9-10 February 2012


Thursday, 9 February
9:15 - 9:30 Welcome
9:30 - 10:30 Mikołaj Bojańczyk Automata with data values and nominal sets
  This talk claims that nominal sets are a unified framework that describes various kinds of automata over data words. Nominal sets are a different kind of set theory, originating in the work of Mostowski and Fraenkel, and appearing in computer science thanks to Gabbay and Pitts. The definition of a set is different, and crucially, the definition of a finite set is different. In the world of nominal sets, for instance, the alphabet used in data words is a finite alphabet. I will show that in nominal sets, the standard definitions of automata yield various kinds of automata for data words, mainly variants of Kaminski and Francez automata.
10:30 - 11:00 Coffee break
11:00 - 11:40 Nikos Tzevelekos Games with names
  This talk is about formal reasoning techniques for programming languages with names which have emerged in the last years. We will focus on game semantics, and in particular nominal game semantics. The latter constitutes a fresh strand of the theory, founded on nominal sets of Gabbay and Pitts, which provides models for programming languages with new resources such as fragments of ML. Moreover, nominal game models can be given algorithmic representations by means of newly introduced abstract machines, called Fresh-Register Automata, which operate on infinite alphabets of names and extend ordinary Register Automata.
11:40 - 12:20 Andrzej Murawski Algorithmic games for ground storage
  We investigate a finitary ML-like language equipped with primitives for storing reference names. Using game semantics and automata-theoretic techniques we provide a complete characterization of cases in which contextual equivalence is decidable.
12:20 - 13:00 Ugo Montanari A network-conscious extension of pi-calculus
  Traditional process calculi usually abstract away from network details, modelling only communication over shared channels. They, however, seem inadequate to describe new network architectures, such as Software Defined Networks, where programs are allowed to manipulate the infrastructure. In this talk we present a network conscious, proper extension of the pi-calculus: we add connector names and primitives to handle them. We also hint to a coalgebraic semantics in the style of Fiore, Turi and Staton, where a saturated semantics is derived categorically. (Joint work with Matteo Sammartino)
13:00 - 14:30 Lunch
14:30 - 15:10 Sławomir Lasota Nominal computation
  This talk is an attempt at defining computation in nominal sets. I present a rudimentary programming language called Nlambda. The key idea is that it includes a native type for finite sets in the nominal sense. To illustrate the power of this language, I write short programs that process automata on data words.
15:10 - 15:50 Ranko Lazic On Petri nets with a stack
  These systems can be seen as models of programs with unbounded integers and recursion, and are also closely related to a first-order logic with two variables on data trees. Atig and Ganty have recently shown that the notion of index of a context-free language can be used to restrict the systems so that they become equivalent to Reinhardt's Petri nets with weak inhibitor arcs, and therefore have decidable reachability. We provide a lower bound for reachability for the unrestricted Petri nets with a stack, whose decidability remains an open problem.
15:50 - 16:30 Coffee break
16:30 - 17:10 Christian Urban Nominal techniques in Isabelle
17:10 - 18:00 Discussion
Friday, 10 February
9:00 - 9:40 Bartek Klin Nominal sets on structured data
  I describe a generalization of nominal sets to a situation where atoms (or data values) come equipped with a first-order relational structure that can be checked upon. Mathematically, this amounts to considering subgroups of data bijections. Some parts of Gabbay-Pitts' theory of nominal sets work without change in this nominal setting. Other parts, such as the existence of least supports, depend on further assumptions on the relational structure in question.
9:40 - 10:20 Szymon Toruńczyk Automata over non-homogeneous structures
  We describe a rudimentary framework for dealing with automata which work over structures which are non-homogeneous, such as (Z,<). The approach is to consider actions of inverse semigroups.
10:20 - 10:50 Coffee break
10:50 - 11:30 Alexander Kurz/Emilio Tuosto On nominal regular languages with binders
  We investigate regular languages on infinite alphabets where words may contain binders on names. To this end, classical regular expressions and automata are extended with binders. We prove the equivalence between finite automata on binders and regular expressions with binders and investigate closure properties and complementation of regular languages with binders.
11:30 - 12:10 Vincenzo Ciancia Stream automata are coalgebras
  Stream automata (also called omega-automata), and omega-regular languages, are of paramount importance in Computer Science and Logic. A coalgebraic treatment of these structures has not been given yet. We study a simple two-sorted setting where deterministic Muller automata can be cast as coalgebras, so that coalgebraic bisimilarity coincides with language equivalence. From this characterisation, we derive concise and natural decision procedures for complementation, union, intersection, and equivalence check. Once a coalgebraic formulation has been established, one may seek for generalisations e.g. by extending the base category. Stream automata over nominal sets would be a direct application of the developed framework.
12:10 - 12:30 Closing remarks
12:30 - 14:00 Lunch