Joshua Moerman

Email

joshua at cs.rwth-aachen.de

Address

Room 4210
Ahornstraße 55
D-52074 Aachen

homepage

https://joshuamoerman.nl

Phone

+49 241 80 21203

I have moved to the Open Universiteit as of 01.05.2021, and so this page won’t be updated anymore. Please visit my personal website. You can also find me on DBLP, Google Scholar, and ORCID.

I was Post-Doc at this chair since April 2019, where I was working on probabilistic programs as a member of the FRAPPANT project.

Research

Formerly, I was a PhD student at the Radboud University in Nijmegen at the Software Science department. Under supervision of Frits Vaandrager, Bas Terwijn, and Alexandra Silva I worked on nominal techniques and black box testing for automata learning.

My research interests also include formal verification, PAC learning, coalgebraic methods, functional programming, black-box testing theory, and category theory.

Bachelor or Master Theses

If you are looking for doing in theses in our group, then I would be happy to supervise you. Here are some ideas for theses. Other topics are of course also possible. Just come by or send an email and then we can talk about it!

• Learning parametric Markov chains. Imagine, there is some parametric Markov chain, but we have no description of it. Can we infer the structure by just looking at its behaviour? Theoretically, this should be learnable to some extend, but there are no implementations. Topics: theory of weighted automata, probability theory, automata learning, a bit of implementation. Some preliminary (and vague) ideas can be found on my blog.
• Duality in automata learning. Duality is ubiquitous in computer science. It gives a correspondence between state transformers and predicate transformer, between forward and backward reasoning in Bayesian networks, between modal logic and state spaces, and so on. Can we leverage this for automata learning? Topics: automata learning, duality theory, a bit of implementation
• Learning MDPs with SMT solving. Can we infer the structure of an Markov decision process (up to equivalence) by only observing its behaviour? Topics: probability theory, SMT solving, implementation.
• What is the probability of finding a counterexample? Black box testing of a finite state machine is the problem of checking equivalence between a specification and implementation by tests only. Surprisingly, this can be done in a sound and complete way (under some assumption), making it a formal method. Can we give quantitative measures to compare different test generation methods? Topics: Black box testing, state machines, probability theory, implementation.
• Gradient Descent for Parametric Markov Chains. Can gradient descent (or another iterative method) be useful for parameter synthesis? I think so, but we will have to implement it and benchmark it. Topics: Markov chains, model checking, implementation. This could be supervised together with Jip Spel. I have written some preliminary (and vague) theory on my blog.

See also this list.

Publications (in RWTH UB)

Publications