\(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs (Q1311976)

The paper contributes to several known results on undecidability of propositional dynamic logics. Two variants of propositional dynamic logic for concurrent programs are proven highly undecidable. These variants are an extension of PDL by the asynchronous constructs shuffle and iterated shuffle (APDL), and a variant of PDL with a partial commutativity relation on primitive programs (CPDL). The validity problem for APDL and CPDL is proven to be \(\Pi^ 1_ 1\)-universal. In both cases the proof is based on simulation of infinite computations of one-counter machines.