PDL with data constants
type: Item
instance of: scholarly article
title: PDL with data constants
zbMATH Open document ID: 0577.68046
DOI: 10.1016/0020-0190(85)90127-9
author: Solomon Passy
author: Tinko Tinchev
published in: Information Processing Letters
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 3924131
zbMATH Keywords: dynamic algebra
zbMATH Keywords: data identity
zbMATH Keywords: undecidability
zbMATH Keywords: verification of
zbMATH Keywords: programs
zbMATH Keywords: propositional dynamic logic
zbMATH Keywords: intersection
zbMATH Keywords: complement
zbMATH Keywords: complete axiomatization
reviewed by: Hirokazu Nishimura
MaRDI profile type: Publication
full work available at URL: 0020-0190(85)90127-9
OpenAlex ID: W2036328670
cites work: Propositional dynamic logic of regular programs
cites work: First-order dynamic logic
cites work: Q3313253
cites work: An elementary proof of the completeness of PDL
cites work: Q3919070
cites work: Q3922159
cites work: Q5596237
cites work: Q5551146
cites work: Q3322087
cites work: Q5734410
description: scientific article; zbMATH DE number 3924131