Title: Dynamic Logic of Propositional Assignments

Speaker: Andreas Herzig (Institut de Recherche en Informatique de Toulouse)

Time: Apr. 21st (Tuesday), 15:10 - 18:00

Location: Room 314, Teaching Building No.2 (北京大学第二教学楼314)

Abstract:

Dynamic Logic of Propositional Assignments (DL-PA) is a variant of PDL whose atomic programs are assignments of propositional variables. In DL-PA, quantification over a propositional variable p can be expressed straightforwardly as nondeterministic choice between assigning p to true and assigning p to false. The other way round, it is less obvious to find a polynomial translation from DL-PA to QBF. We start by eliminating the Kleene star; then put formulas into a normal form where all modal operators correspond to boolean quantifiers; and finally prenex quantifiers in a polynomial way. 

Based on ongoing work with Abdallah Saffidine (paper on arXiv).