Intuitionistic LTL and a New Characterization of Safety and Liveness

Patrick Maier

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

28 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages295-309
Number of pages15
Volume3210
DOIs
Publication statusPublished - 2004
EventComputer Science Logic - Karpacz, Poland
Duration: 20 Sept 200424 Sept 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Conference

ConferenceComputer Science Logic
Abbreviated title CSL 2004
Country/TerritoryPoland
CityKarpacz
Period20/09/0424/09/04

Keywords

  • 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