
We present an Angluinstyle algorithm to learn nominal automata, which are
acceptors of languages over infinite (structured) alphabets. The abstract
approach we take allows us to seamlessly extend known variations of the
algorithm to this new setting. In particular we can learn a subclass of nominal
nondeterministic automata. An implementation using a recently developed
Haskell library for nominal computation is provided for preliminary
experiments.

Automata learning has been successfully applied in the verification of
hardware and software. The size of the automaton model learned is a bottleneck
for scalability, and hence optimizations that enable learning of compact
representations are important. This paper exploits monads, both as a
mathematical structure and a programming construct, to design, prove correct,
and implement a wide class of such optimizations. The former perspective on
monads allows us to develop a new algorithm and accompanying correctness
proofs, building upon a general framework for automata learning based on
category theory. The new algorithm is parametric on a monad, which provides a
rich algebraic structure to capture nondeterminism and other sideeffects. We
show that our approach allows us to uniformly capture existing algorithms,
develop new ones, and add optimizations. The latter perspective allows us to
effortlessly translate the theory into practice: we provide a Haskell library
implementing our general framework, and we show experimental results for two
specific instances: nondeterministic and weighted automata.

Automata learning is a technique that has successfully been applied in
verification, with the automaton type varying depending on the application
domain. Adaptations of automata learning algorithms for increasingly complex
types of automata have to be developed from scratch because there was no
abstract theory offering guidelines. This makes it hard to devise such
algorithms, and it obscures their correctness proofs. We introduce a simple
categorytheoretic formalism that provides an appropriately abstract foundation
for studying automata learning. Furthermore, our framework establishes formal
relations between algorithms for learning, testing, and minimization. We
illustrate its generality with two examples: deterministic and weighted
automata.

In this paper we revisit some pioneering efforts to equip Petri nets with
compact operational models for expressing causality. The models we propose have
a bisimilarity relation and a minimal representative for each equivalence
class, and they can be fully explained as coalgebras on a presheaf category on
an index category of partial orders. First, we provide a settheoretic model in
the form of a a causal case graph, that is a labeled transition system where
states and transitions represent markings and firings of the net, respectively,
and are equipped with causal information. Most importantly, each state has a
poset representing causal dependencies among past events. Our first result
shows the correspondence with behavior structure semantics as proposed by
Trakhtenbrot and Rabinovich. Causal case graphs may be infinitelybranching and
have infinitely many states, but we show how they can be refined to get an
equivalent finitelybranching model. In it, states are equipped with
symmetries, which are essential for the existence of a minimal, often
finitestate, model. The next step is constructing a coalgebraic model. We
exploit the fact that events can be represented as names, and event generation
as name generation. Thus we can apply the FioreTuri framework: we model causal
relations as a suitable category of posets with action labels, and generation
of new events with causal dependencies as an endofunctor on this category. Then
we define a wellbehaved category of coalgebras. Our coalgebraic model is still
infinitestate, but we exploit the equivalence between coalgebras over a class
of presheaves and History Dependent automata to derive a compact
representation, which is equivalent to our settheoretical compact model.
Remarkably, state reduction is automatically performed along the equivalence.

Many optimization problems can be naturally represented as (hyper) graphs,
where vertices correspond to variables and edges to tasks, whose cost depends
on the values of the adjacent variables. Capitalizing on the structure of the
graph, suitable dynamic programming strategies can select certain orders of
evaluation of the variables which guarantee to reach both an optimal solution
and a minimal size of the tables computed in the optimization process. In this
paper we introduce a simple algebraic specification with parallel composition
and restriction whose terms up to structural axioms are the graphs mentioned
above. In addition, free (unrestricted) vertices are labelled with variables,
and the specification includes operations of name permutation with finite
support. We show a correspondence between the wellknown tree decompositions of
graphs and our terms. If an axiom of scope extension is dropped, several
(hierarchical) terms actually correspond to the same graph. A suitable
graphical structure can be found, corresponding to every hierarchical term.
Evaluating such a graphical structure in some target algebra yields a dynamic
programming strategy. If the target algebra satisfies the scope extension
axiom, then the result does not depend on the particular structure, but only on
the original graph. We apply our approach to the parking optimization problem
developed in the ASCENS emobility case study, in collaboration with
Volkswagen. Dynamic programming evaluations are particularly interesting for
autonomic systems, where actual behavior often consists of propagating local
knowledge to obtain global knowledge and getting it back for local decisions.

We define a class of languages of infinite words over infinite alphabets, and
the corresponding automata. The automata used for recognition are a
generalisation of deterministic Muller automata to the setting of nominal sets.
Remarkably, the obtained languages are determined by their ultimately periodic
fragments, as in the classical case. Closure under complement, union and
intersection, and decidability of emptiness and equivalence are preserved by
the generalisation. This is shown by using finite representations of the
(otherwise infinitestate) defined class of automata.