Intuitionistic LTL and a New Characterization of Safety and Liveness

Patrick Maier

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

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 Sep 200424 Sep 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Conference

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

Fingerprint

Temporal logic

Keywords

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

Cite this

Maier, P. (2004). Intuitionistic LTL and a New Characterization of Safety and Liveness. In 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
Maier, Patrick. / Intuitionistic LTL and a New Characterization of Safety and Liveness. Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL; Karpacz, Poland, September 20-24, 2004; Proceedings. Vol. 3210 Springer, 2004. pp. 295-309 (Lecture Notes in Computer Science).
@inproceedings{c2b0e4e2dda54bc9ab859e8962c7892a,
title = "Intuitionistic LTL and a New Characterization of Safety and Liveness",
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.",
keywords = "linear-time temporal logic, intuitionistic logic, safety and liveness properties",
author = "Patrick Maier",
year = "2004",
doi = "10.1007/978-3-540-30124-0_24",
language = "English",
volume = "3210",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "295--309",
booktitle = "Computer Science Logic",

}

Maier, P 2004, Intuitionistic LTL and a New Characterization of Safety and Liveness. in 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.

Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL; Karpacz, Poland, September 20-24, 2004; Proceedings. Vol. 3210 Springer, 2004. p. 295-309 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference 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 -

Maier P. Intuitionistic LTL and a New Characterization of Safety and Liveness. In Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL; Karpacz, Poland, September 20-24, 2004; Proceedings. Vol. 3210. Springer. 2004. p. 295-309. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-30124-0_24