∏11-universality of some propositional logics of concurrent programs

AbstractIt is proved that validity problems for two variants of propositional dynamic logic (PDL) connected with concurrent programming are highly undecidable (∏11-universal). These variants are an extension of PDL by asynchronous programming constructs shuffle and iterated shuffle and a variant of PDL with a partial commutativity relation on primitive programs. In both cases propositional variables are not used