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 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)

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

• 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?)
• A near-optimal method for reasoning about action
• 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

(35)

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

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)