© 1996-2019

| | | ||

| ## 3.3 ITL library for Isabelle/HOLIsabelle/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 embedding of propositional ITL and a shallow embedding of ﬁrst order 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., [96] for a discussion about deep vs. shallow embeddings in Isabelle/HOL. The shallow embedding of ﬁrst order ITL uses techniques developed by Stefan Merz [175, 20] for the shallow embedding of Temporal Logic of Actions (TLA) in Isabelle/HOL. - Deep embedding:
Contains: - Propositional ITL, syntax, semantics (ﬁnite 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” have been veriﬁed.
- Link with Georg Struths work on Kleene Algebra. This work is based on Interval Temporal Algebra (Section 3.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.
Download: - Version 1.10 (11/06/2019), gzipped tar ﬁle.
Changes: - Replaced notation deprecated in Isabelle/HOL 2019.
- Version 1.9 (16/03/2019), gzipped tar ﬁle.
Changes: - Restructure First and Monitor Theories.
- Added equivalence relation on monitors.
- See ChangeLog for detailed changes.
- Version 1.8 (08/12/2018, ﬁrst public release), gzipped tar ﬁle.
- Shallow embedding:
Contains: - First Order ITL, both quantiﬁcation over state variables, added temporal variables (current, next, ﬁnal, penultimate), syntax, semantics, and axioms and proof rules. The technique used is similar to that of Stephan Merz [175, 20] used for encoding 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 also works for temporal variables and quantiﬁcation.
- First operator and Monitors. All key theorems/lemmas/semantics in David Smallwood PhD thesis “ITL Monitor: Compositional Runtime Analysis with Interval Temporal Logic” have been veriﬁed.
- Some concrete monitors have been speciﬁed and properties veriﬁed.
- Some examples using quantiﬁcation.
Download: - Version 2.4 (11/06/2019, still work in progress), gzipped tar ﬁle.
Changes: - Replaced notation deprecated in Isabelle/HOL 2019.
- Version 2.3 (16/03/2019, still work in progress), gzipped tar ﬁle.
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 ﬁle.
| | ||

| |