\(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs (Q1311976)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 487966
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs |
scientific article; zbMATH DE number 487966 |
Statements
\(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs (English)
0 references
12 December 1994
0 references
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.
0 references
concurrency
0 references
undecidability
0 references
propositional dynamic logic
0 references
iterated shuffle
0 references
partial commutativity relations on primitive programs
0 references
validity problem
0 references
infinite computations of one-counter machines
0 references
0 references
0 references
0.7868363857269287
0 references
0.7798667550086975
0 references
0.7780390381813049
0 references
0.7748921513557434
0 references
