\(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs (Q1311976): Difference between revisions
From MaRDI portal
Removed claim: reviewed by (P1447): Item:Q282093 |
Changed an Item |
||
Property / reviewed by | |||
Property / reviewed by: Luboš Brim / rank | |||
Normal rank |
Revision as of 13:23, 12 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs |
scientific article |
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