Propositional dynamic logic of nonregular programs

DOI10.1016/0022-0000(83)90014-4MaRDI QIDQ792083zbMATH OpenOpenAlexFDO

Authors David Harel, Amir Pnueli, Jonathan Stavi

Publication date 1983

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0022-0000(83)90014-4

zbMATH Keywords

context-free grammarcontext-free PDLdecidabilitypropositional dynamic logicrecursive programs

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Modal logic (including the logic of norms) (03B45) Other nonclassical logic (03B60) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

It was shown by \textit{M. J. Fischer} and \textit{R. E. Ladner} [J. Comput. Syst. Sci. 18, 194-211 (1979; Zbl 0408.03014)] that the validity problem for regular propositional dynamic logic (PDL) is decidable in deterministic exponential time, and, within a polynomial, this upper bound is the best possible. The authors consider similar problems for context-free PDL, showing that the borderline between decidable and undecidable PDL is extremely close to the original regular PDL, and strikingly that the transition leaps from decidability in exponential time for regular PDL to \(\Pi^ 1_ 1\)-completeness. A comprehensive characterization of the class of programs for which PDL is decidable remains an intriguing topic for future research.

Recommendations

• Undecidability of PDL with \(L=\{a^{2^ i}| i\geq 0\}\)
• Deciding Properties of Nonregular Programs
• scientific article; zbMATH DE number 3848600
• The propositional dynamic logic of deterministic, well-structured programs
• Propositional dynamic logic with recursive programs

Cites work

• A near-optimal method for reasoning about action
• scientific article; zbMATH DE number 3174044 (Why is no real title available?)
• scientific article; zbMATH DE number 3862425 (Why is no real title available?)
• scientific article; zbMATH DE number 3731325 (Why is no real title available?)
• scientific article; zbMATH DE number 3772937 (Why is no real title available?)
• scientific article; zbMATH DE number 3539209 (Why is no real title available?)
• scientific article; zbMATH DE number 3639163 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• On the completeness of the inductive assertion method
• Propositional dynamic logic of regular programs
• Superdeterministic PDAs
• The decidability of equivalence for a family of linear grammars
• Two decidability results for deterministic pushdown automata

Cited in

(37)

• Communication in concurrent dynamic logic
• The complexity of reasoning about knowledge and time. I: Lower bounds
• Programming in metric temporal logic
• \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs
• A theory of timed automata
• Mathematical modal logic: A view of its evolution
• The price of universality
• More on nonregular PDL: Finite models and Fibonacci-like programs
• Temporal logic with recursion
• Verification of concurrent programs: The automata-theoretic framework
• Model checking propositional dynamic logic with all extras
• Propositional dynamic logic with recursive programs
• Classes of timed automata and the undecidability of universality
• Well-structured program equivalence is highly undecidable
• Proving the decidability of the \(\mathrm{PDL}\times\mathrm{PDL}\) product logic
• Deciding Properties of Nonregular Programs
• Propositional dynamic logic for reasoning about first-class agent interaction protocols
• scientific article; zbMATH DE number 3848600 (Why is no real title available?)
• scientific article; zbMATH DE number 3862425 (Why is no real title available?)
• scientific article; zbMATH DE number 4154413 (Why is no real title available?)
• A note on definability in fragments of arithmetic with free unary predicates
• Regular dynamic logic is not interpretable in deterministic context-free dynamic logic
• Collapsing probabilistic hierarchies. I
• Branching-time logics with path relativisation
• Decision complexity of variants of propositional dynamic logic
• Presburger arithmetic with unary predicates is Π₁¹ complete
• Decidability and incompleteness results for first-order temporal logics of linear time
• Propositional dynamic logic with program quantifiers
• Products of ‘transitive” modal logics
• Temporal Logic with Recursion.
• Model checking timed recursive CTL
• Separating the expressive power of propositional dynamic and modal fixpoint logics
• Regular model checking for systems with effectively regular reachability relation
• The propositional dynamic logic of deterministic, well-structured programs
• Undecidability of PDL with \(L=\{a^{2^ i}| i\geq 0\}\)
• Propositional dynamic logic of context-free programs and fixpoint logic with chop
• A note on an extension of PDL

This page was built for publication: Propositional dynamic logic of nonregular programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q792083)