Automata in Learning, Interaction and Concurrency (ALICE)

The ALICE project is funded by the Estonian Research Council grant PRG1210.

Abstract

As software becomes ever more ubiquitous and interconnected, our theoretical models must also become more expressive and robust. Formal languages and automata theory are a foundation of computer science, while at the same time enjoying a myriad of practical applications. This project will extend and exploit classical automata theory along three dimensions, addressing challenges characterizing large and complex software systems.

Senior staff

Open positions



PhD scholarship 1

Theory and practice of symbolic automata

Supervisors: Dr. Hellis Tamm and Dr. Hendrik Maarand

Description

Symbolic finite automata [1,2] extend classical automata by allowing infinite alphabets. Indeed *predicates* over such 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.

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,5]. Also, the role of atoms of regular languages [4,5] in the symbolic setting will be explored.

  • [1] D’Antoni, L., Veanes, M.: The power of symbolic automata and transducers. CAV 2017. LNCS 10426, 47–67, Springer. 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, 620--635, ACM. doi: 10.1145/3453483.3454066
  • [4] Brzozowski, J.A., Tamm, H.: Theory of atomata. Theor. Comput. Sci. 539, 13–27 (2014) doi: 10.1016/j.tcs.2014.04.016
  • [5] Tamm, H., Veanes, M.: Theoretical aspects of symbolic automata. SOFSEM 2018. LNCS 10706, 428-441, Springer. doi: 10.1007/978-3-319-73117-9_30

Applicants should be highly motivated and ideally have some previous knowledge of automata theory. For more information and/or to apply online, visit https://taltech.glowbase.com/positions/424

PhD scholarship 2

Algebraic theories of cellular automata over concrete categories

Supervisors: Dr. Silvio Capobianco and Dr. Tarmo Uustalu

Description:

Cellular automata (CA) are an example of context-dependent computation, which can be modeled as coKleisli maps of comonads or, more generally, arrows. In a CA, entities occupy the nodes of a grid which has a group of translations, and their state, taken from an alphabet, is updated synchronously according to a local rule (coKleisli map); this induces a global function (coalgebra) which updates the state of the entire grid. If the group or the alphabet have special properties, these can reflect into special properties of the rules.

The project will develop and implement a framework for CA over concrete categories whose objects can "reasonably" be seen as sets. More in general, we will study cellular automata over value spaces with algebraic structure, e.g. an abelian group. Local computations can be required to be linear or additive and this ensures that so is also the global computation (the coKleisli extension of the coKleisli map). This framework will expand on the ideas from Capobianco and Uustalu (2010) and Behrisch et al. (2017).

A first nontrivial example of CA on a concrete category is given by linear CA, where the alphabet is a ring and the local rule (equivalently, the global function) is linear: these are precisely the CA on the concrete category of modules over the given ring. It is known (Sato (1993)) that reversibility and surjectivity of linear CA over finite commutative rings are decidable in arbitrary dimension, and correspond to algebraic properties of the Laurent polynomial describing the local rule. A first step in the project can then be a translation of this fact in the language of category theory.

The PhD student will be affiliated with the ALICE (Automata in Learning, Interaction and Concurrency) group, Department of Software Science, TalTech. The ALICE project aims at extending and exploiting classical automata theory for the requirements of modern software.

Applicants should fulfil the following requirements:

  • MSc in Mathematics, Computer Science, or related field.
  • Previous experience with category theory and/or cellular automata theory.
For more information and/or to apply online, visit https://taltech.glowbase.com/positions/426 for Estonian applicants, including graduants of Estonian universities and https://taltech.glowbase.com/positions/427 for international applicants
  • [1] Mike Behrisch, Sebastian Kerkhoff, Reinhard Pöschel, Friedrich Martin Schneider, Stefan Siegmund. Dynamical Systems in Categories. Applied Categorical Structures 25 (2017), 29--57. https://doi.org/10.1007/s10485-015-9409-8 Preprint: https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa-129909
  • [2] Silvio Capobianco and Tarmo Uustalu. A categorical outlook on cellular automata. In J. Kari, ed., Proc. of 2nd Symp. on Cellular Automata, JAC 2010 (Turku, Dec. 2010), v. 13 of TUCS Lecture Notes, pp. 88--99. Turku Centre for Computer Science, 2010. https://hal.archives-ouvertes.fr/hal-00542015
  • [3] Tullio Ceccherini-Silberstein and Michel Coornaert. Cellular Automata and Groups. Springer, 2010.
  • [4] Tullio Ceccherini-Silberstein and Michel Coornaert. Surjunctivity and reversibility of cellular automata over concrete categories. In: Picardello M. (eds) Trends in Harmonic Analysis. Springer INdAM Series, vol 3. Springer, Milano. doi:10.1007/978-88-470-2853-1_6 Preprint: arXiv:1203.6492
  • [5] John Hughes. Generalising monads with arrows. Science of Computer Programming. 37 (1–3): 67–111. doi:10.1016/S0167-6423(99)00023-4
  • [6] Jarkko Kari. Theory of cellular automata: a survey. Theoretical Computer Science 334 (2005) 3--33.
  • [7] Tadakazu Sato. Decidability of some problems of linear cellular automata over finite commutative rings. Information Processing Letters, 46:151–155, 1993.

Meetings

Our hybrid meetings are held on Fridays 11:00am in the 4th floor coffee room of the Cybernetics building, and on Zoom, at this link.

Presentations

  • Silvio Capobianco, A category theory approach to the theory of dynamical systems, Tuesday 22 June 2021, 11:00-12:00

    Abstract: In the broadest definition, dynamical systems are actions of monoids over spaces. Several models in logic and computer science, such as finite automata, Turing machines, and cellular automata, can be described as dynamical systems. All of those can be seen as either computations or processes, and the latter can in turn be seen as algebras and coalgebras, respectively, in suitable categories.

    This talk explores an approach to dynamical system through category theory, in particular the theory of (co)monads. The base for it will be the paper by Behrisch et al. (2017). Possible applications to the theory of cellular automata will also be discussed.

  • Tarmo Uustalu, Interaction laws of (perhaps not only) monads, April 9 2021

    Abstract: I will recap interaction laws of monads and comonads (Katsumata, Rivas, U., LICS 2020). They are a means to specify how computations within a notion of effectful computation described by some monad can run in environments. They admit an elegant mathematical theory because of the duoidal structure of endofunctor categories (composition and the Day convolution). I will speculate on the question of if similar accounts of running could be possible for notions of computation described, instead of monads, by related structures such as "applicative functors", "arrows" or relative monads.

  • Margus Veanes, Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints, March 12 2021

    Abstract: The manipulation of raw string data is ubiquitous in security-critical software, and verification of such software relies on efficiently solving string and regular expression constraints via SMT. However, the typical case of Boolean combinations of regular expression constraints exposes blowup in existing techniques. To address solvability of such constraints, we propose a new theory of derivatives of symbolic extended regular expressions (extended meaning that complement and intersection are incorporated), and show how to apply this theory to obtain more efficient decision procedures. Our implementation of these ideas, built on top of Z3, matches or outperforms state-of-the-art solvers on standard and handwritten benchmarks, showing particular benefits on examples with Boolean combinations.

    Our work is the first formalization of derivatives of regular expressions which both handles intersection and complement and works symbolically over an arbitrary character theory without requiring mintermization. It unifies existing approaches involving derivatives of extended regular expressions, alternating automata and Boolean automata by lifting them to a common symbolic platform. It relies on a parsimonious augmentation of regular expressions: a construct for symbolic conditionals is shown to be sufficient to obtain relevant closure properties for derivatives over extended regular expressions.

    Link to TR (accepted to PLDI'2021):

  • Silvio Capobianco, Cellular automata and comonads: An overview , March 05 2021 -- slides.

    Abstract: Cellular automata (CA) are a parallel model of computation, where a regular grid of identical finite automata is updated by synchronous application of a local rule, the next state of a node being a function of the current state of a neighborhood defined by a list of offsets. These features suggest a formalization in category theory via comonads. A comonad on a category is a monad on the opposite category. Comonads are suited to describe processes in the same way monads are suited to describe computations. In this talk, we will discuss a formalization of CA in terms of comonads, which Tarmo Uustalu and I presented at JAC 2010. Remarkably, local rules correspond to morphisms in the coKleisli category, and global functions correspond to cofree coalgebras in the coEilenberg-Moore category. With this formalization, some basic theorems of CA theory follow from general facts about comonads. Some possible future directions will also be discussed.

  • Hendrik Maarand, Introduction to Symbolic Automata, February 19 2021.

    Abstract: Symbolic automata were developed as an extension of classical automata to allow infinite alphabets and to improve the handling of large alphabets. In this talk, we will first look at basic properties of symbolic automata and then we will consider minimisation of automata to highlight some aspects of working with symbolic automata.

  • Hellis Tamm, Atoms of Regular Languages and Finite Automata, February 5 2021