An expanded version of Semantics for Linear-time Temporal Logic with Finite Observations.

Linear-time temporal properties, such as those described by Linear-time Temporal Logic, are typically modelled as sets of infinite traces. Yet, in a run-time verification context, such as when testing or monitoring a system, only a finite prefix of the system’s behaviour can be observed. For some properties, these finite prefixes may be definitive—a yes or no answer can be given without further observation. By enriching the semantics of LTL with these definitive prefixes, we give a proper inductive accounting of the semantics of LTL3, a multi-valued variant of Linear-time Temporal Logic for run-time verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of their relationship to conventional LTL. We show that the semantics of LTL and of LTL3 are isomorphic. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification contexts, and show its soundness and completeness up to finite traces with respect to our semantics. Then, we turn to linear-time properties more generally: using our theory of definitive prefixes, we re-prove the well-known safety-liveness decomposition theorem, and reconstruct the topology of infinite traces. We define monitorability for properties, providing neat topological characterisations for various monitorability classes, and arrange them into a hierarchy. All of our definitions and proofs are mechanised in Isabelle/HOL.

The literature on runtime “verification” (the activity of monitoring a running process to ensure compliance with a given specification) offers many different definitions of “monitorability” for properties. In a linear-time temporal setting, properties take the form of sets of behaviours (infinite sequences of states). In this talk, I will arrange the various monitorability classes found in the literature into a hierarchy along with well-known classes of properties such as safety and guarantee properties. I then give each of these monitorability classes neat topological characterisations within the topology induced by the "guarantee kernel" interior operator. Lastly, I show that the metric space used by Alpern and Schneider coincides with our topology.

We define a proper inductive semantics for LTL which includes those finite partial traces for which a definitive answer can be given: the “definitive prefixes” of the property. Sets of definitive prefixes are called definitive sets. Defining a semantics for LTL in terms of definitive sets gives us something equivalent to LTL3, a formulation popular in runtime verification. Our theory of definitive sets is sufficient to give a neat characterisation of (co-)safety and (co-)liveness properties, allowing us to straightforwardly prove Alpern and Schneider’s result that every property is the intersection of a safety and liveness property by simpler means.

LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. Our approach, by contrast, gives a full model-based inductive accounting of the semantics of LTL3, in terms of families of definitive prefix sets. We show that our definitive prefix sets are isomorphic to linear-time temporal properties (sets of infinite traces), and thereby show that our semantics of LTL3 directly correspond to the semantics of conventional LTL. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics. All of our definitions and proofs are mechanised in Isabelle/HOL.

In this talk I demonstrated how the well known Zipper structure of Huet, later generalised by McBride, can be used to equip any modal logic with inverse modalities. In particular, this allows us to equip any temporal logic, including CTL, with a notion of linear past.

Rewriting is a versatile and powerful technique used in many domains. Strategic rewriting allows programmers to control the application of rewrite rules by composing individual rewrite rules into complex rewrite strategies. These strategies are semantically complex, as they may be nondeterministic, they may raise errors that trigger backtracking, and they may not terminate.

Given such semantic complexity, it is necessary to establish a formal understanding of rewrite strategies and to enable reasoning about them in order to answer questions like: How do we know that a rewrite strategy terminates? How do we know that a rewrite strategy does not fail because we compose two incompatible rewrites? How do we know that a desired property holds after applying a rewrite strategy?

In this paper, we introduce Shoggoth: a formal foundation for understanding, analysing and reasoning about strategic rewriting that is capable of answering these questions. We provide a denotational semantics of System S, a core language for strategic rewriting, and prove its equivalence to our big-step operational semantics, which extends existing work by explicitly accounting for divergence. We further define a location-based weakest precondition calculus to enable formal reasoning about rewriting strategies, and we prove this calculus sound with respect to the denotational semantics. We show how this calculus can be used in practice to reason about properties of rewriting strategies, including termination, that they are well-composed, and that desired postconditions hold. The semantics and calculus are formalised in Isabelle/HOL and all proofs are mechanised.

In this talk I give whirlwind tour of denotational semantics, an oft-neglected but very important branch of theoretical computer science, which truly connects computer programs to mathematics