PDL with data constants. (English) Zbl 0577.68046
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.
Reviewer: H.Nishimura
MSC:
| 68Q65 | Abstract data types; algebraic specification |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
dynamic algebra; data identity; undecidability; verification of; programs; propositional dynamic logic; intersection; complement; complete axiomatizationReferences:
| [1] | Fischer, M.; Ladner, R., Propositional modal logic of programs, J. Comput. Syst. Sci., 18, 194-211 (1979) · Zbl 0408.03014 |
| [2] | G. Gargov, Personal communication, 1984.; G. Gargov, Personal communication, 1984. |
| [3] | Harel, D., First order dynamic logic, (Lecture Notes in Computer Science, 68 (1979), Springer: Springer Berlin) · Zbl 0403.03024 |
| [4] | Harel, D., Recurring dominoes: Making in highly undecidable highly understandable, (Lecture Notes in Computer Science, 158 (1983), Springer: Springer Berlin), 177-194 · Zbl 0531.68002 |
| [5] | Kozen, D.; Parikh, R., An elementary completeness proof for PDL, Theoret. Comput. Sci., 14, 113-118 (1981) · Zbl 0451.03006 |
| [6] | Meyer, A.; Streett, R. S.; Mirkowska, G., The deducibility problem in propositional dynamic logic, (Lecture Notes in Computer Science, 125 (1981), Springer: Springer Berlin), 12-22 · Zbl 0466.68024 |
| [7] | Passy, S.; Tinchev, T., Data constants in PDL: The natural state affairs (1984), Submitted |
| [8] | Parikh, R., Propositional dynamic logics of programs: A survey, (Lecture Notes in Computer Science, 125 (1981), Springer: Springer Berlin), 102-144 · Zbl 0468.68038 |
| [9] | Pratt, V., Semantical consideration on Floyd-Hoare logic, (Proc. 17th Ann. IEEE Symp. on Foundations of Computer Science (1976)), 109-121 |
| [10] | Pratt, V., Dynamic algebras: Examples, constructions, applications, Rept. MIT/LCS/TM-138 (1979) |
| [11] | Salwicki, A., Formalized algorithmic languages, Bull. Acad. Pol. Sci., Ser. Sci. Math., Astr. et Phys., XVIII, 5, 227-232 (1970) · Zbl 0198.02801 |
| [12] | Scott, D., A logic with denumerable long formulas and finite strings of quantifiers, (Addison, J.; etal., The Theory of Models, Proc. 1963 Symp. at Berkeley (1965/1970/1972), North-Holland: North-Holland Amsterdam), 329-342 · Zbl 0166.26003 |
| [13] | Segerberg, K., A completeness theorem in modal logic of programs, Preliminary Rept., Notices AMS, 24, 6, A-552 (1977) |
| [14] | Skordev, D., Combinatory Spaces and Recursiveness in Them (1980), Publ. House of the Bulg. Acad. of Sci: Publ. House of the Bulg. Acad. of Sci Sofia · Zbl 0537.03029 |
| [15] | Rasiowa, H.; Sikorski, R., The Mathematics of Meta-mathematics (1963), PWN: PWN Warszawa · Zbl 0122.24311 |
| [16] | Tinchev, T.; Vakarelov, D., PDL with least fixed points which are programs, (Abstract presented at Summer School on Mathematical Logic. Abstract presented at Summer School on Mathematical Logic, Primorsko (1983), Publ. House of the Bulg. Acad. of Sci: Publ. House of the Bulg. Acad. of Sci Sofia) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
