PROJECT: Comparing Regular Expressions
Supervisor: M. Bonsangue

Regular expressions are an important and well-known instrument
for describing lexical tokens in syntax specifications and text
patterns in text manipulation systems. In this project, the
candidate will have to learn several novel construction and
implement a framework for comparing regular expressions based
on non-deterministic finite automata. This is contrast to the
classical solution due to Thompson based on non-deterministic
finite automata with lambda-transitions.

PROJECT: Model Checking and Synthesis of Sequential Digital Circuits
Supervisor: M. Bonsangue

In present day text books on logic design -— on the
construction of sequential digital circuits -— Mealy machines
are still the most important mathematically exact means for the
specification of the intended behaviour of circuits. There does
not seem to exist, however, a generally accepted way of
formally specifying Mealy machines themselves. In this project
the candidate will learn a simple but adequate and expressive
logical language for the specification of Mealy machines. Here
adequate means that the logical equivalence corresponds to a
natural behavioural equivalence on Mealy machines, whereas
expressive means that every finite Mealy machine can be
represented by a (finite) formula. Finally, simple means that
the logic contains precisely what is needed to obtain this
goal, and nothing more. Extension of the logic with useful
specification constructs as well as the implementation of the
Model Checking and Synthesis algorithms constitute the novel
parts of this project.

PROJECT: Model Checking and Synthesis of Software Circuits
Supervisor: M. Bonsangue

Reo is a graphical language resembling that of sequential
digital circuits for the exogenous composition and
orchestration of components in a software system. An
operational model of Reo connectors can be given in terms of
Buchi automata over a suitable alphabet of records, capturing
both synchronization and context dependency requirements. In
this project, the candidate will study an action based variant
linear time temporal logic for expressing properties of Reo
connectors. The goal is to define efficent algorithm for the
synthesis of formulas into g Reo connectors, thus leading to an
automata based model checking algorithm.