Propositional dynamic logic of context-free programs and fixpoint logic with chop. (English) Zbl 1185.68391
Summary: This paper compares propositional dynamic logic of non-regular programs and fixpoint logic with chop. It identifies a fragment of the latter which is equi-expressive to the former. This relationship transfers several decidability and complexity results between the two logics.
MSC:
| 68Q45 | Formal languages and automata |
References:
| [1] | Fischer, M. J.; Ladner, R. E., Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, 18, 2, 194-211 (1979) · Zbl 0408.03014 |
| [2] | Harel, D.; Pnueli, A.; Stavi, J., Propositional dynamic logic of nonregular programs, Journal of Computer and System Sciences, 26, 2, 222-243 (1983) · Zbl 0536.68041 |
| [3] | Harel, D.; Singerman, E., More on nonregular PDL: Finite models and Fibonacci-like programs, Information and Computation, 128, 2, 109-118 (1996) · Zbl 0856.68131 |
| [4] | Hopcroft, J.; Ullman, J., Introduction to Automata Theory, Languages, and Computation (1980), Addison-Wesley: Addison-Wesley N. Reading, MA |
| [5] | Koren, T.; Pnueli, A., There exist decidable context free propositional dynamic logics, (Clarke, E.; Kozen, D., Proc. of the Workshop on Logics of Programs. Proc. of the Workshop on Logics of Programs, Pittsburgh, PA. Proc. of the Workshop on Logics of Programs. Proc. of the Workshop on Logics of Programs, Pittsburgh, PA, Lecture Notes in Computer Science, vol. 164 (1983), Springer-Verlag: Springer-Verlag Berlin), 290-312 · Zbl 0542.68020 |
| [6] | Kozen, D., Results on the propositional \(μ\)-calculus, TCS, 27, 333-354 (December 1983) · Zbl 0553.03007 |
| [7] | Lange, M., Model checking propositional dynamic logic with all extras, Journal of Applied Logic, 4, 1, 39-49 (2005) · Zbl 1095.68053 |
| [8] | M. Lange, Three notes on the complexity of model checking fixpoint logic with chop, RAIRO—Theoretical Informatics and Applications, 2006, in press; M. Lange, Three notes on the complexity of model checking fixpoint logic with chop, RAIRO—Theoretical Informatics and Applications, 2006, in press · Zbl 1133.68046 |
| [9] | Löding, C.; Serre, O., Propositional dynamic logic with recursive programs, (Proc. 9th Int. Conf. on Foundations of Software Science and Computation Structures. Proc. 9th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS’06. Proc. 9th Int. Conf. on Foundations of Software Science and Computation Structures. Proc. 9th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS’06, Lecture Notes in Computer Science, vol. 3921 (2006), Springer-Verlag: Springer-Verlag Berlin), 292-306 · Zbl 1180.03034 |
| [10] | Müller-Olm, M., A modal fixpoint logic with chop, (Meinel, C.; Tison, S., Proc. 16th Symp. on Theoretical Aspects of Computer Science. Proc. 16th Symp. on Theoretical Aspects of Computer Science, STACS’99, Trier, Germany. Proc. 16th Symp. on Theoretical Aspects of Computer Science. Proc. 16th Symp. on Theoretical Aspects of Computer Science, STACS’99, Trier, Germany, Lecture Notes in Computer Science, vol. 1563 (1999), Springer: Springer Berlin), 510-520 · Zbl 0924.03046 |
| [11] | Pratt, V. R., Semantical considerations on Floyd-Hoare logic, (17th Annual Symp. on Foundations of Computer Science. 17th Annual Symp. on Foundations of Computer Science, FOCS’76, Houston, TX (1976), IEEE: IEEE New York), 109-121 |
| [12] | Tarski, A., A lattice-theoretical fixpoint theorem and its application, Pacific Journal of Mathematics, 5, 285-309 (1955) · Zbl 0064.26004 |
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.
