Propositional dynamic logic of nonregular programs

DOI10.1016/0022-0000(83)90014-4zbMath0536.68041OpenAlexW2062879749MaRDI QIDQ792083

David Harel, Jonathan Stavi, Amir Pnueli

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

decidabilitycontext-free grammarpropositional dynamic logicrecursive programscontext-free PDL

Mathematics Subject Classification ID

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) Decidability of theories and sets of sentences (03B25)

Related Items (24)

Communication in concurrent dynamic logic ⋮ Propositional dynamic logic of context-free programs and fixpoint logic with chop ⋮ Presburger arithmetic with unary predicates is Π₁¹ complete ⋮ Decidability and incompleteness results for first-order temporal logics of linear time ⋮ Propositional dynamic logic with recursive programs ⋮ The complexity of reasoning about knowledge and time. I: Lower bounds ⋮ A note on definability in fragments of arithmetic with free unary predicates ⋮ Programming in metric temporal logic ⋮ Collapsing probabilistic hierarchies. I ⋮ Branching-time logics with path relativisation ⋮ PROPOSITIONAL DYNAMIC LOGIC FOR REASONING ABOUT FIRST-CLASS AGENT INTERACTION PROTOCOLS ⋮ Mathematical modal logic: A view of its evolution ⋮ Temporal Logic with Recursion. ⋮ Products of ‘transitive” modal logics ⋮ A note on an extension of PDL ⋮ Propositional Dynamic Logic with Program Quantifiers ⋮ Model checking propositional dynamic logic with all extras ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Temporal logic with recursion ⋮ The price of universality ⋮ Classes of Timed Automata and the Undecidability of Universality ⋮ Undecidability of PDL with \(L=\{a^{2^ i}| i\geq 0\}\) ⋮ \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs ⋮ A theory of timed automata

Cites Work

• A near-optimal method for reasoning about action
• On the completeness of the inductive assertion method
• Two decidability results for deterministic pushdown automata
• Propositional dynamic logic of regular programs
• Superdeterministic PDAs
• The decidability of equivalence for a family of linear grammars
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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