PDL with data constants (Q1065545)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | PDL with data constants |
scientific article |
Statements
PDL with data constants (English)
0 references
1985
0 references
This paper considers an extension of classical propositional dynamic logic with new operators for programs such as \(\alpha\) \(\cap \beta\) (the intersection of the programs \(\alpha\) and \(\beta)\) and \({\bar \alpha}\) (the complement of the program \(\alpha)\) and new formulas such as \(\alpha\) \(\subset \beta\) and \(\alpha =\beta\), which is given an (infinitary) complete axiomatization and shown to be highly undecidable.
0 references
dynamic algebra
0 references
data identity
0 references
undecidability
0 references
verification of
0 references
programs
0 references
propositional dynamic logic
0 references
intersection
0 references
complement
0 references
complete axiomatization
0 references
