2018/03/13 by Philippe Balbiani, Joseph Boudou, Balbiani, Philippe +4
Computer Science · #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1803.05078
openalex publication_date 2018/03/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We introduce bisimulations for the logic ITLe with `next', `until' and\n`release', an intuitionistic temporal logic based on structures equipped with a\npartial order used to interpret intuitionistic implication and a monotone\nfunction used to interpret the temporal modalities. Our main results are that\n`eventually', which is definable in terms of `until', cannot be defined in\nterms of `next' and `henceforth', and similarly that `henceforth', definable in\nterms of `release', cannot be defined in terms of `next' and `until', even over\nthe smaller class of here-and-there models.\n