» Apply now PDF Show all positions


Symbolic finite automata extend classical automata by allowing infinite alphabets. In these automata predicates over infinite alphabets, which form a Boolean algebra, serve as labels of transitions. Symbolic automata have been studied intensively in recent years, because they solve some practical problems for which classical finite automata are unsuitable. However, the study of symbolic automata is a young field and much work is still to be done.

Research field: Information and communication technology
Supervisors: Prof. Dr. Pawel Sobocinski
Dr. Hellis Tamm
Availability: This position is available.
Offered by: School of Information Technologies
Department of Software Science
Application deadline:Applications are accepted between June 01, 2022 00:00 and June 30, 2022 23:59 (Europe/Zurich)


This PhD project explores theoretical as well as practical aspects of symbolic automata. The project will advance symbolic automata research, studying classes of finite automata (e.g. residual automata, reversible automata, boolean automata) in the symbolic setting [3,4], especially focussing on automata learning [5].


[1] D’Antoni, L., Veanes, M.: The power of symbolic automata and transducers. CAV 2017. doi: 10.1007/978-3-319-63387-9_3 [2] D'Antoni, L., Veanes, M.: Automata modulo theories. Commun. ACM, 64, 5, 86-95, 2021, doi: 10.1145/3419404

[3] Stanford, C., Veanes, M., Bjørner, N.: Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. PLDI 2021, doi: 10.1145/3453483.3454066

[4] Tamm, H., Veanes, M.: Theoretical aspects of symbolic automata. SOFSEM 2018. doi: 10.1007/978-3-319-73117-9_30

[5] Argyros, G., D'Antoni L. The learnability of symbolic automata. CAV 2018. doi: 10.1007/978-3-319-96145-3_23


The project will form a part of an ongoing Estonian Research Council project PRG1210, Automata in Learning, Interaction and Concurrency (ALICE), and will also involve collaboration with Margus Veanes, Microsoft Research (Redmond). Applicants should be highly motivated and ideally have some previous knowledge of automata theory.