Automata@FIT research group

Automata@FIT is a research group at FIT BUT, founded in 2023, focusing on research around finite automata and related formalisms, their theory, the fundamental principles needed to use them efficiently in applications, and the applications themselves: in formal automatic reasoning, system analysis and verification, deciding logics, SMT-solving, string constraint solving, analysis of quantum circuits, in regular pattern recognition, network monitoring and anomaly detection, formalisms and methods to deal with uncertainty and to support automated decision making.

Current Research

We currently focus on

• development of string constraint solving technology, based on finite automata, with applications in the analysis of string manipulation systems, web application vulnerabilities, security policy analysis, e.g. cloud technologies,
• analysis of quantum circuits using techniques based on tree automata
• automatic procedures for decision logics such as integer linear arithmetic, WS1S, MSO, HyperLTL
• development of general-purpose techniques and tools for efficient use of finite automata
• development of concise extensions to finite automata and decision diagrams and methods for working with them (e.g., alternations, registers, counters, procedures)
• Markov models as a formalism for dealing with uncertainty and supporting automated decision making
• automata in network traffic monitoring and anomaly detection
• efficient regular pattern matching