Microsoft Research, Redmond, WA
Monday, 26 September 2016, 10:00 (note the unusual weekday and time)
IT Bldg (Akadeemia tee 15A), room 411
Slides from the talk [pptx]
Abstract: Symbolic finite automata or SFAs extend classical automata by allowing transitions to carry predicates over an effective Boolean algebra, instead of concrete labels. In this talk, we discuss the main algorithmic properties of SFAs and illustrate some of their applications. We focus in more detail on one application that is to use SFAs as a backend for a symbolic extension of the weak monadic second-order logic of one successor. The extension is to allow character predicates to range over decidable alphabets instead of finite alphabets. We present a decision procedure for this logic based on a reduction to SFAs. An important part of the reduction is the use of Cartesian products of Boolean algebras. We show how one can use a variant of algebraic decision diagrams to implement Cartesian products of Boolean algebras.