### Abstract

Original language | English |
---|---|

Title of host publication | Computer Science Logic |

Subtitle of host publication | 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL; Karpacz, Poland, September 20-24, 2004; Proceedings |

Publisher | Springer |

Pages | 295-309 |

Number of pages | 15 |

Volume | 3210 |

DOIs | |

Publication status | Published - 2004 |

Event | Computer Science Logic - Karpacz, Poland Duration: 20 Sep 2004 → 24 Sep 2004 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

### Conference

Conference | Computer Science Logic |
---|---|

Abbreviated title | CSL 2004 |

Country | Poland |

City | Karpacz |

Period | 20/09/04 → 24/09/04 |

### Fingerprint

### Keywords

- linear-time temporal logic
- intuitionistic logic
- safety and liveness properties

### Cite this

*Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL; Karpacz, Poland, September 20-24, 2004; Proceedings*(Vol. 3210, pp. 295-309). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-540-30124-0_24

}

*Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL; Karpacz, Poland, September 20-24, 2004; Proceedings.*vol. 3210, Lecture Notes in Computer Science, Springer, pp. 295-309, Computer Science Logic, Karpacz, Poland, 20/09/04. https://doi.org/10.1007/978-3-540-30124-0_24

**Intuitionistic LTL and a New Characterization of Safety and Liveness.** / Maier, Patrick.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Intuitionistic LTL and a New Characterization of Safety and Liveness

AU - Maier, Patrick

PY - 2004

Y1 - 2004

N2 - Classical linear-time temporal logic (LTL) is capable of specifying of and reasoning about infinite behaviors only. While this is appropriate for specifying non-terminating reactive systems, there are situations (e.g. assume-guarantee reasoning, run-time verification) when it is desirable to be able to reason about finite and infinite behaviors. We propose an interpretation of the operators of LTL on finite and infinite behaviors, which defines an intuitionistic temporal logic (ILTL). We compare the expressive power of LTL and ILTL. We demonstrate that ILTL is suitable for assume-guarantee reasoning and for expressing properties that relate finite and infinite behaviors. In particular, ILTL admits an elegant logical characterization of safety and liveness properties.

AB - Classical linear-time temporal logic (LTL) is capable of specifying of and reasoning about infinite behaviors only. While this is appropriate for specifying non-terminating reactive systems, there are situations (e.g. assume-guarantee reasoning, run-time verification) when it is desirable to be able to reason about finite and infinite behaviors. We propose an interpretation of the operators of LTL on finite and infinite behaviors, which defines an intuitionistic temporal logic (ILTL). We compare the expressive power of LTL and ILTL. We demonstrate that ILTL is suitable for assume-guarantee reasoning and for expressing properties that relate finite and infinite behaviors. In particular, ILTL admits an elegant logical characterization of safety and liveness properties.

KW - linear-time temporal logic

KW - intuitionistic logic

KW - safety and liveness properties

U2 - 10.1007/978-3-540-30124-0_24

DO - 10.1007/978-3-540-30124-0_24

M3 - Conference contribution

VL - 3210

T3 - Lecture Notes in Computer Science

SP - 295

EP - 309

BT - Computer Science Logic

PB - Springer

ER -