Propositional dynamic logic of nonregular programs

DOI10.1016/0022-0000(83)90014-4zbMATH Open0536.68041OpenAlexW2062879749MaRDI QIDQ792083FDOQ792083

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

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

zbMATH Keywords

context-free grammardecidabilitypropositional dynamic logicrecursive programscontext-free PDL

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Propositional dynamic logic of regular programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the completeness of the inductive assertion method
• A near-optimal method for reasoning about action
• Title not available (Why is that?)
• Two decidability results for deterministic pushdown automata
• Title not available (Why is that?)
• Superdeterministic PDAs
• Title not available (Why is that?)
• The decidability of equivalence for a family of linear grammars
• Title not available (Why is that?)

Cited In (35)

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

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)