Bisimulations for intuitionistic temporal logics

03/14/2018
by   Philippe Balbiani, et al.
0

We introduce bisimulations for the logic ITL^e with `next', `until' and `release', an intuitionistic temporal logic based on structures equipped with a partial order used to interpret intuitionistic implication and a monotone function used to interpret the temporal modalities. Our main results are that `eventually', which is definable in terms of `until', cannot be defined in terms of `next' and `henceforth', and similarly that `henceforth', definable in terms of `release', cannot be defined in terms of `next' and `until', even over the smaller class of here-and-there models.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset