There are various proposals in the process-algebraic literature for extending process algebra with a notion of signal [1,2]. In those proposals processes can emit (partial) information about their state to other processes without resorting to the message passing paradigm. There are several theoretical open questions pertaining these proposals. For instance, to what extent do the addition of signals increase the expressiveness of the process algebra, and is the equational theory presented in [1] sound and ground-complete for rooted branching bisimilarity. Furthermore, it would be interesting to develop the theory of a process algebra with data and signals. This could serve as a stepping stone towards and extension of mCRL2 with a notion of shared variable.

In [1], a finite ω-complete axiomatisation of the equational theory of the process algebra PA was presented. One of the axioms needed in this axiomatisation is not sound if the constant 1 (denoting immediate successful termination) is added to the theory. The assignment is to investigate whether a finite ω-complete axiomatisation exists for the extension of PA with the constant 1.

The mCRL2 toolset uses term rewriting to generate state spaces before applying model checking algorithms. Since these state spaces are huge, it is important to have fast term rewriting. An important subproblem of rewriting is the term pattern matching problem: given a set of term/tree patterns we want to quickly discover the set of matches in a term. We have published a paper that describes set automata [2] to tackle this problem. From the set of left-hand sides of a rewrite system we generate a set automaton that can be used to scan any term for pattern matches. Construction of a set automaton is done as a preprocessing step before state space generation. Using this method, we look at every symbol of the input term only once. There are several open questions that we are interested in. A graduation project consists of tackling one or more of these problems.

1. Failure link set automata

   Set automata generalize the well-known Aho-Corasick string matching algorithm [2]. Aho and Corasick actually describe two versions of their algorithm. The less-known version builds a fully specified automaton from a pattern set. That is, for every state and every symbol there is an outgoing edge. Set automata are also fully specified, so they generalize this version. However, the signatures that we use tend to have a lot of symbols, which makes the automaton generation and storage expensive.

   The best-known version of the Aho-Corasick algorithm only has transitions that occur in the trie associated to the pattern set. For non-matching symbols it specifies failure links, only one for every state, that take you back in the trie. Whenever there is no outgoing transition for a symbol, we follow the failure link, and then try the same symbol again until we succeed in some state, or fail in the initial state. The question is, can we build a set automaton with failure links rather than a fully specified automaton?

2. Optimized Automaton construction

   The definition of set automata in our paper is theoretically sound, but it is rather complicated and expensive. We encode every state with every possible subterm that we can still encounter, and apply some mathematical tricks to get a finite state machine. The question is, how can we optimize automaton construction?

3. Linear time matching

   Set automata require some look-ahead to operate correctly. To observe one symbol from a certain position in a set automaton, we may have to look very deeply from a current root. We observe every symbol only once, but observing a symbol takes at most d time where d is the maximal depth of any term pattern. Total complexity of pattern matching is then O(dn+m) where n is the amount of symbols in the input term and m is the amount of pattern matches. The question is, given the set automaton, can we run the matching algorithm in O(n+m) time?

   [1]	Aho, A. V., & Corasick, M. J. (1975). Efficient string matching: an aid to bibliographic search. Communications of the ACM, 18(6), 333-340.
   [2]	Erkens, R., & Groote, J. F. (2021). A set automaton to locate all pattern matches in a term. In International Colloquium on Theoretical Aspects of Computing (pp. 67-85). Springer, Cham.