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
T2 - Computer Science Logic
Y2 - 20 September 2004 through 24 September 2004
ER -