Author name cluster

Joshua Moerman

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

TCS Journal 2022 Journal Article

Fast computations on ordered nominal sets

David Venhoek
Joshua Moerman
Jurriaan Rot

Nominal automata are models for recognising languages over infinite alphabets, based on the algebraic notion of nominal set. Motivated by their use in automata theory, we show how to compute efficiently with nominal sets over the so-called total order symmetry, a variant which allows to compare alphabet letters for equality as well as their respective order. We develop an explicit finite representation of such nominal sets and basic constructions thereon. The approach is implemented as the library Ons (Ordered Nominal Sets), enabling programming with infinite sets. Returning to our motivation of nominal automata, we evaluate Ons in two applications: minimisation of automata and active automata learning. In both cases, Ons is competitive compared to existing implementations and outperforms them for certain classes of inputs.

Details DOI

LOPSTR Conference 2020 Conference Paper

Generating Functions for Probabilistic Programs

Lutz Klinkenberg
Kevin Batz
Benjamin Lucien Kaminski
Joost-Pieter Katoen
Joshua Moerman
Tobias Winkler 0001

Abstract This paper investigates the usage of generating functions (GFs) encoding measures over the program variables for reasoning about discrete probabilistic programs. To that end, we define a denotational GF-transformer semantics for probabilistic while-programs, and show that it instantiates Kozen’s seminal distribution transformer semantics. We then study the effective usage of GFs for program analysis. We show that finitely expressible GFs enable checking super-invariants by means of computer algebra tools, and that they can be used to determine termination probabilities. The paper concludes by characterizing a class of—possibly infinite-state—programs whose semantics is a rational GF encoding a discrete phase-type distribution.

Details

Highlights Conference 2020 Conference Abstract

Residuality and Learning for Register Automata

Joshua Moerman

In this research we consider the problem of inferring a register automaton from observations. This has been done before for deterministic RA, but is still open for nondeterministic RA. To see why nondeterminism is interesting, consider the well-known learning algorithms L* and NL* for respectively deterministic and nondeterministic automata. Although the representation is different, they operate on the same class of languages (i. e. , regular languages). This is not the case for RA, where nondeterminism gives a strictly bigger class of languages than determinism. So not only does the representation changes, so does the class of languages. Our contributions are as follows. This is joint work with Matteo Sammartino. – We consider \emph{residual automata} for data languages. We show that their languages form a proper subclass of all languages accepted by nondeterministic RA. – we give a \emph{machine-independent characterisation} of this class of languages. For this, we also develop some new results in nominal lattice theory. – We show that for this class of languages, L*-style algorithms exist. – The natural generalisation of NL* does not always terminate, surprisingly. Fortunately, the algorithm can be fixed to always terminate.

Details

CSL Conference 2020 Conference Paper

Separation and Renaming in Nominal Sets

Joshua Moerman
Jurriaan Rot

Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e. g. , to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

Details