Propositional dynamic logic of looping and converse is elementarily decidable
Information and ControlPublished 1 July 1982
Robert S. Streett
Citations211
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
It is proved that the satisfiability problem for propositional dynamic logic of looping and converse is elementarily decidable and deterministic two- way automata on infinite trees are defined and it is shown how they can be simulated by nondeterministic one-way automata.
Abstract
Propositional dynamic logic is a formal system for reasoning about the before—after behavior of regular program schemes. An extension of propositional dynamic logic which includes both an infinite looping construct and a converse or backtracking construct is considered and it is proved that the satisfiability problem for this logic is elementarily decidable. In order to establish this result, deterministic two-way automata on infinite trees are defined, and it is shown how they can be simulated by nondeterministic one-way automata. The satisfiability problem for propositional dynamic logic of looping and converse is then reduced to the emptiness problem for these two-way automata.
Keywords
Computer Science
Journal of Computer and System SciencesPropositional dynamic logic of regular programs
1,191 Citations1979Michael J. Fischer, Richard E. Ladner
A formal syntax and semantics for the propositional dynamic logic of regular programs is defined and principal conclusions are that deciding satisfiability of length n formulas requires time d n /log n for some d > 1, and that satisfiability can be decided in nondeterministic time cn for some c.
Transactions of the American Mathematical SocietyDecidability of second-order theories and automata on infinite trees.
1,159 Citations1969Michael O. Rabin
Journal of Symbolic LogicVaughan R. Pratt. Semantical considerations on Floyd–Hoare logic. 17th Annual Symposium on Foundations of Computer Science, Institute of Electrical and Electronics Engineers, New York1976, pp. 109–121. - Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of computer and system sciences, vol. 18 (1979), pp. 194–211. - Krister Segerberg. A completeness theorem in the modal logic of programs. Universal algebra and applications. Papers presented at Stefan Banach International Mathematical Center at the semester “Universal algebra and applications” held February 15–June 9, 1978, edited by Tadeuz Traczyk, Banach Center Publications, vol. 9, PWN—Polish Scientific Publishers, Warsaw1982, pp. 31–46. - Rohit Parikh. The completeness of propositional dynamic logic. Mathematical foundations of computer science 1978, Proceedings, 7th symposium, Zakopane, Poland, September 4–8, 1978, edited by J. Winkowski, Lecture notes in computer science, vol. 64, Springer-Verlag, Berlin, Heidelberg, and New York, 1978, pp. 403–415. - Dexter Kozen and Rohit Parikh. An elementary proof of the completeness of PDL. Theoretical computer science, vol. 14(1981), pp. 113–118.
429 Citations1986Robert Goldblatt
An appropriate axiom system is given which is complete for loop-free programs and also puts conventional predicate calculus in a different light by lumping quantifiers with non-logical assignments rather than treating them as logical concepts.
Lecture notes in computer scienceResults on the propositional μ-calculus
251 Citations1982Dexter Kozen
A propositional version of the Μ-calculus is defined, and an exponential-time decision procedure, small model property, and complete deductive system is given, and it is shown that it is strictly more expressive than PDL.
Models of program logics
200 Citations1979Vaughan Pratt
The common theory has already been shown to be complete in deterministic exponential time; the simpler proof of the upper bound is given.
Propositional Dynamic Logic of looping and converse
152 Citations1981Robert S. Streett
Propositional Dynamic Logic can be extended to include both an infinitary iteration construct delta and a backtracking construct converse, and the resulting logic does not satisfy the finite model property, but is nevertheless elementarily decidable.
Theoretical Computer ScienceFiniteness is mu-ineffable
95 Citations1976David Park
The "mu-calculus" is a formal system which arises fairly naturally when one tries to extend predicate logic to formalise arguments about programs.
A decidable mu-calculus: Preliminary report
88 Citations1981Vaughan Pratt
This work provides an intimate link between PDL as defined by the Segerberg axioms and the mu-calculi of de Bakker and Park and shows that its satisfiability problem is decidable in exponential time.
A decidability result for a second order process logic
53 Citations1978Rohit Parikh
The decidability of the validity problem for a rather general language for talking about computations is proved and some decidable results of Pratt, Constable, Fischer-Ladner, and Pnueli are obtained.
The emptiness problem for automata on infinite trees
42 Citations1972R. Hossley, Charles Rackoff
The proof reduces the emptiness problem for automata on infinite trees to that for Automata on finite trees, by showing that any automata definable set of infinite trees must contain a finitely-generable tree.
Complete axiomatization of algorithmic properties of program schemes with bounded nondeterministic interpretations
12 Citations1980Grażyna Mirkowska
It is proved that the semantical and the syntactical consequence operations coincide (completeness property) and that the model existence theorem holds.
DSpace@MIT (Massachusetts Institute of Technology)Applications of Modal Logic to Programming
1 Citations1978Pratt, Vaughan R.