POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 16:30 - 16:55 at Amphitheater 44 - Logic Chair(s): Alexandra Silva

We extend the weak monadic second-order logic of one successor on finite strings (M2L-STR) to symbolic alphabets by allowing character predicates to range over decidable quantifier free theories instead of finite alphabets. We call this logic, which is able to describe sequences over complex and potentially infinite domains, symbolic M2L-STR (S-M2L-STR). We then present a decision procedure for S-M2L-STR based on a reduction to symbolic finite automata, a decidable extension of finite automata that allows transitions to carry predicates and can therefore model symbolic alphabets. The reduction constructs a symbolic automaton over an alphabet consisting of pairs of symbols where the first element of the pair is a symbol in the original formula’s alphabet, while the second element is a bit-vector. To handle this modified alphabet we show that the Cartesian product of two decidable Boolean algebras (e.g., the formula’s one and the bit-vector’s one) also forms a decidable Boolean algebras. To make the decision procedure practical, we propose two efficient representations of the Cartesian product of two Boolean algebras, one based on algebraic decision diagrams and one on a variant of Shannon expansions. Finally, we implement our decision procedure and evaluate the performance of our implementation on a comprehensive set of formulas.

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:45: LogicPOPL at Amphitheater 44
Chair(s): Alexandra SilvaUniversity College London
16:30 - 16:55
Monadic second-order logic on finite sequences
Loris D'AntoniUniversity of Wisconsin–Madison, Margus VeanesMicrosoft Research
16:55 - 17:20
On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
Naoki KobayashiUniversity of Tokyo, Japan, Etienne LozesENS Cachan, Florian BruseUniversity of Kassel
17:20 - 17:45
Coming to Terms with Quantified Reasoning
Simon RobillardChalmers University of Technology, Andrei VoronkovUniversity of Manchester, Laura KovacsChalmers University of Technology