Well-structured program equivalence is highly undecidable

DOI10.1145/2287718.2287726MaRDI QIDQ2946675zbMATH OpenOpenAlexFDO

Authors Robert Goldblatt, Marcel Jackson

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1103.1433

zbMATH Keywords

deterministic propositional dynamic logicfixsetintersectionPDLprogram equivalenceundecidability

Mathematics Subject Classification ID

Logic in computer science (03B70) Undecidability and degrees of sets of sentences (03D35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Abstract: We show that strict deterministic propositional dynamic logic with intersection is highly undecidable, solving a problem in the Stanford Encyclopedia of Philosophy. In fact we show something quite a bit stronger. We introduce the construction of program equivalence, which returns the value $mathsfT$ precisely when two given programs are equivalent on halting computations. We show that virtually any variant of propositional dynamic logic has $P{i}_1^1$-hard validity problem if it can express even just the equivalence of well-structured programs with the empty program exttt{skip}. We also show, in these cases, that the set of propositional statements valid over finite models is not recursively enumerable, so there is not even an axiomatisation for finitely valid propositions.

Recommendations

• Propositional dynamic logic of nonregular programs
• \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs
• Propositional dynamic logic with recursive programs
• The propositional dynamic logic of deterministic, well-structured programs
• PDL with data constants

Cited in

(8)

• \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs
• Monoids with tests and the algebra of possibly non-halting programs
• Static analysis of navigational XPath over graph databases
• Halting and equivalence of program schemes in models of arbitrary theories
• scientific article; zbMATH DE number 1738658 (Why is no real title available?)
• On axiomatizations of public announcement logic
• Undecidability of the positive calculus of relations with transitive closure and difference: hypothesis elimination using graph loops
• The algebra of functions with antidomain and range

This page was built for publication: Well-structured program equivalence is highly undecidable

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