Logic and Automata

There is a tight connection between certain logics and automata which can be used, for example, to devise decision procedures for problems in software verification.

Expressive Power

The study of the expressive power of various formalisms is a central topic in mathematics. In our group we investigate the expressive power of certain logics using tools from logic, automata theory, and algebra. The focus lies on monadic second-order logic and its fragments over infinite trees and various graph classes.

Automata Engineering

Automata on infinite words are cornerstones of many algorithms for verification, analysis, or synthesis of reactive systems. We study translation of linear temporal logic (LTL) to classes of automata with various structural properties (e.g., deterministic, nondeterministic) and acceptance conditions (e.g., Büchi, Emerson-Lei, parity). Further, we develop techniques for efficient automata reductions and transformations, and also algorithms processing automata.

SMT Solving

Satisfiability modulo theory (SMT) solving studies algorithms deciding whether a given formula is satisfiable in a given theory. These algorithms are implemented in SMT solvers, which have numerous applications. We primarily focus on SMT solving of bitvector theory, which is a crucial component of many program analysis tools based on bounded model checking or symbolic execution. 

What We Do

No description

Study Formalisms

  • We study expressive power of various logics and automata classes.
  • We analyze decidability and complexity of relevant problems.  
No description

Algorithms & Experiments

  • We develop algorithms for creation, reduction, transformation, and application of automata.
  • We propose algorithms for satisfiability and SMT solving.
  • We make intensive experiments to assess the efficiency of our algorithms compared to other existing approaches.
No description

Tools & Software

  • LTL3TELA - translator of LTL to Emerson-Lei automata
  • Seminator - tool for semideterminization and complementation of automata
  • Q3B - SMT solver for quantified bitvector formulas

Our Team

Join Us

Want to contribute to any part of our mission? Looking for a bachelor or master thesis topic? Interested in obtaining a Ph.D. degree? Join us!  


You are running an old browser version. We recommend updating your browser to its latest version.

More info