Expressive completeness failure in branching time structures

DOI10.1016/0022-0000(87)90003-1MaRDI QIDQ1109759zbMATH OpenOpenAlexFDO

Authors Amihood Amir

Publication date 1987

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(87)90003-1

zbMATH Keywords

branching timeexpressive completenessfunctional completenesstense logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Review text

As for the expressive completeness problem (or equivalently, functional completeness problem) of tense logics, all the logics over linear time and some over non-linear time structures have already been shown affirmatively by the author and others. Gabbay, on the other hand, has proved that the general time structure is not expressively complete. In this paper, the author extends the negative case by proving that an infinite tree with an unbounded branching factor is not expressively complete.

Recommendations

• Expressive completeness of temporal logic of trees
• Correct Hardware Design and Verification Methods
• Decision procedures and expressiveness in the temporal logic of branching time
• Completeness of a branching-time logic with possible choices
• Transition semantics for branching time
• Branching within time: An expressively complete and elementarily decidable temporal logic for time granularity
• scientific article; zbMATH DE number 177795
• scientific article; zbMATH DE number 1222565
• Incompleteness of first-order temporal logic with until
• Branching time and abstraction in bisimulation semantics

Cites work

• scientific article; zbMATH DE number 3827831 (Why is no real title available?)
• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 3263218 (Why is no real title available?)
• Investigations in modal and tense logics with applications to problems in philosophy and linguistics

Cited in

(2)

• Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs?
• Separation in nonlinear time models

This page was built for publication: Expressive completeness failure in branching time structures

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