Intuitionistic LTL and a New Characterization of Safety and Liveness

Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL; Karpacz, Poland, September 20-24, 2004; Proceedings
Number of pages15
Publication statusPublished - 2004
EventComputer Science Logic - Karpacz, Poland
Duration: 20 Sep 200424 Sep 2004

Publication series

NameLecture Notes in Computer Science


ConferenceComputer Science Logic
Abbreviated title CSL 2004


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

Fingerprint Dive into the research topics of 'Intuitionistic LTL and a New Characterization of Safety and Liveness'. Together they form a unique fingerprint.

Cite this