Theory and Practice of Symbolic Automata
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.
Information and communication technology|
Prof. Dr. Pawel Sobocinski|
Dr. Hellis Tamm
|Availability:||This position is available.|
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 .
 D’Antoni, L., Veanes, M.: The power of symbolic automata and transducers. CAV 2017. doi: 10.1007/978-3-319-63387-9_3  D'Antoni, L., Veanes, M.: Automata modulo theories. Commun. ACM, 64, 5, 86-95, 2021, doi: 10.1145/3419404
 Stanford, C., Veanes, M., Bjørner, N.: Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. PLDI 2021, doi: 10.1145/3453483.3454066
 Tamm, H., Veanes, M.: Theoretical aspects of symbolic automata. SOFSEM 2018. doi: 10.1007/978-3-319-73117-9_30
 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.