4.3 ITL library for Isabelle/HOL
Isabelle/HOL is a generic proof assistant. It allows mathematical formulas to be expressed in a formal
language and provides tools for proving those formulas in a logical calculus.
We have given a deep and shallow embedding of several variants of ITL in Isabelle/HOL. A shallow
embedding represents ITL using Isabelle/HOL predicates, while a deep embedding would represent
ITL formulas as mutually inductive datatypes. See, e.g., [106] for a discussion about deep vs.
shallow embeddings in Isabelle/HOL. The shallow embedding of ITL uses techniques developed
by Stefan Merz [192, 24] for the shallow embedding of Temporal Logic of Actions (TLA) in
Isabelle/HOL.
4.3.1 Finite and Infinite ITL, shallow and deep embedding
- Intervals are denoted by non-empty coinductive lists. These are a subtype of coinductive lists
formalised by Andreas Lochbihler [26].
- First Order ITL, both quantification over state variables, temporal variables (current, next,
final, penultimate), syntax, semantics, and axioms and proof rules. The encoding is similar to
that of Stephan Merz [192, 24] used for TLA in Isabelle/HOL.
- The lemmas from Imperative Reasoning in Interval Temporal Logic by Ben Moszkowski.
- The until operator for finite and infinite ITL and extensive list of lemmas from [189].
- The Pi operator [83, 4] for finite and infinite ITL.
- Finite and Infinite Interval Temporal Algebra. This work is based on Interval Temporal Algebra
(Section 4.4) but now re-encoded in Isabelle/HOL. So the work on ITL and Prover9 and PVS
has now been superseded by the Isabelle/HOL library. ITA is related to Kleene and Omega
Algebras [13].
- A deep embedding of PITL (propositional ITL), QPITL (PITL with quantifiers), NL-ITL
(QPITL with neighbourhood operators [2]) and CDT-PITL (PITL with CDT operators of [51]
but without chopstar and chop-omega). NL-ITL and CDT-PITL are examples of an expanding
logic which can refer to states outside the current interval whereas traditional ITL is an
introspective logic which can only refer to states in the current interval.
Download:
-
Version 3.5 (18/03/2025) gzipped tar file Changes:
- Deep embedding of NL-ITL, QPITL with neighbourhood operators [2]. Note, we have
both infinite past and infinite future, therefore we need the theory of extended integers.
This is an example of expanding logic whereas traditional ITL is an introspective logic.
- Deep embedding of CDT-PITL, PITL with the CDT operators of Yde Venema [51] without
chop-star and chop-omega. Another example of an expanding logic.
- Minor changes to existing theory files.
-
Version 3.4 (26/05/2024) gzipped tar file
Changes:
- Deep embedding of PITL and QPITL is included to allow for proofs of theorems about
them, notably that any PITL or QPITL formula can be rewritten in Guarded Normal
Form (GNF) [2, 34].
- Added definition and lemmas for the time reversal operator, ported from the ITL v2.x
series. Note only finite ITL formula can be reversed.
- The document structure is now report with four chapters: 1 Model: Intervals; 2 Shallow
embedding of Finite and Infinite ITL; 3 Deep embedding of PITL; 4 Deep embedding of
QPITL.
-
Version 3.3 (13/09/2023) gzipped tar file
Changes:
- Fixes for Isabelle 2023.
- Ported first and monitor operator definitions and lemmas from the ITL v2.x series.
-
Version 3.2 (26/10/2022) gzipped tar file
Changes:
- Ported the finite projection operator definitions and lemmas from ITLv2.x series (finite
ITL) to infinite ITL. Added infinite projection operator definition and lemmas.
- Added remaining lemmas for chopstar and Pi from [4]. Added lemma for omega and Pi.
- Added womega (Omega operation from Omega Algebra) definition and lemmas, these are
ported from [13]. Added corresponding lemmas for omega (omega from ITL) definition.
Added aomega (semantic version) definition and lemma stating the equivalence with the
omega definition.
- Added wpowerstar (Kleene star operation from Kleene Algebra) definition and lemmas,
these are ported from [13]. Added corresponding lemmas for schopstar (strong schopstar
from ITL) definition. Added achopstar (semantic version) definition and lemma stating
the equivalence with the schopstar definition. Added inductive definition istar and various
lemmas related them to schopstar and wpowerstar.
- Moved all chopstar related definitions and lemmas into a separate theory file.
- Moved all omega related definitions and lemmas into a separate theory file.
-
Version 3.1 (14/12/2021) gzipped tar file
Changes:
- Incorporate changes for Isabelle2021-1.
- Version 3.0 (09/04/2021, first public release) gzipped tar file
4.3.2 Finite ITL, shallow embedding
- First Order finite ITL, both quantification over state variables, temporal variables (current,
next, final, penultimate), syntax, semantics, and axioms and proof rules. The encoding is similar
to that of Stephan Merz [192, 24] used for TLA in Isabelle/HOL.
- The lemmas from Imperative Reasoning in Interval Temporal Logic by Ben Moszkowski.
- Time Reversal operator and an extensive list of lemmas included. Time reversal operator is
also defined for temporal variables and quantification.
- First operator and Monitors. All key theorems/lemmas/semantics in David Smallwood PhD
thesis “ITL Monitor: Compositional Runtime Analysis with Interval Temporal Logic” [166]
have been verified.
- The projection operator [139] for finite ITL.
- Finite Interval Temporal Algebra. This work is based on Interval Temporal Algebra (Section
4.4) but now re-encoded in Isabelle/HOL. So the work on ITL and Prover9 and PVS has now
been superseded by the Isabelle/HOL library. ITA is related to Kleene Algebras [13].
- The until and since operator for finite ITL and extensive list of lemmas from [189].
- The Pi operator [83, 4] for finite ITL.
- Forward and backward executability of ITL formula.
Download:
-
Version 2.9 (26/05/2024) gzipped tar file
Changes:
- Incorporate change for Isabelle 2024.
-
Version 2.8 (14/12/2021) gzipped tar file
Changes:
- Incorporate changes for Isabelle 2021-1.
-
Version 2.7 (28/02/2021) gzipped tar file
Changes:
- Added theory on executability of ITL formulae.
- Naming of definitions and lemmas is more consistent, all operations on intervals are
starting with i.
- Removed infinite ITL, i.e., this version only deals with finite ITL. Infinite and finite ITL
are now in the upcoming version 3.X which uses a uniform representation for finite and
infinite intervals using coinductive lists.
-
Version 2.6 (16/04/2020) gzipped tar file
Changes:
- Added projection operator (for finite ITL), axioms and proof rules.
- Added filter operator on finite intervals and extensive list of lemmas.
- Added until and since operator (for finite ITL) and extensive list of lemmas.
- Added Pi operator (for finite ITL), axiom and proof rules.
- Added Interval Temporal Algebra (for finite ITL) from version 1.
-
Version 2.5 (21/07/2019, more polished version), axioms gzipped tar file.
Changes:
- Added Infinite intervals, semantics, axioms and proof rules, and extensive list of lemmas.
-
Version 2.4 (11/06/2019, still work in progress), gzipped tar file.
Changes:
- Replaced notation deprecated in Isabelle/HOL 2019.
-
Version 2.3 (16/03/2019, still work in progress), gzipped tar file.
Changes:
- Use Intensional.thy from Isabelle/HOL distribution.
- Restructure First and Monitor Theories.
- Added equivalence relation on monitors.
- Restructure Example Theory.
- See ChangeLog for detailed changes.
- Version 2.2 (08/12/2018, warning this is work in progress), gzipped tar file.
4.3.3 Finite ITL, deep embedding
- Propositional ITL, syntax, semantics (finite intervals), and axioms and proof rules.
- The lemmas from Imperative Reasoning in Interval Temporal Logic by Ben Moszkowski.
- Time Reversal operator and an extensive list of lemmas.
- First operator and Monitors. All key theorems/lemmas/semantics in David Smallwood PhD
thesis “ITL Monitor: Compositional Runtime Analysis with Interval Temporal Logic” [166]
have been verified.
- Interval Temporal Algebra for finite interval. This work is based on Interval Temporal Algebra
(Section 4.4) but now re-encoded in Isabelle/HOL. So the work on ITL and Prover9 and PVS
has now been superseded by the Isabelle/HOL library. ITA is related to Kleene Algebras [13].
Download:
-
Version 1.10 (11/06/2019), gzipped tar file.
Changes:
- Replaced notation deprecated in Isabelle/HOL 2019.
-
Version 1.9 (16/03/2019), gzipped tar file.
Changes:
- Restructure First and Monitor Theories.
- Added equivalence relation on monitors.
- See ChangeLog for detailed changes.
- Version 1.8 (08/12/2018, first public release), gzipped tar file.