Hostname: page-component-74656f9884-rngvg Total loading time: 0 Render date: 2026-11-06T01:16:09.917Z Has data issue: false hasContentIssue false
  • English
  • Français

Regular relations for temporal propositions

Published online by Cambridge University Press:  21 March 2011

TIM FERNANDO
TIM FERNANDO*
Affiliation:
Trinity College Dublin, Ireland e-mail: tim.fernando@cs.tcd.ie
Rights & Permissions [Opens in a new window]

Abstract

Relations computed by finite-state transducers are applied to interpret temporal propositions in terms of strings representing finite contexts or situations. Carnap–Montague intensions mapping indices to extensions are reformulated as relations between strings that can serve as indices and extensions alike. Strings are related according to information content, temporal span and granularity, the bounds on which reflect the partiality of natural language statements. That partiality shapes not only strings-as-extensions (indicating what statements are about) but also strings-as-indices (underlying truth conditions).

Information

Type
Papers
Information
Natural Language Engineering , Volume 17 , Special Issue 2: Finite-State Methods and Models in Natural Language Processing , April 2011 , pp. 163 - 184
Copyright
Copyright © Cambridge University Press 2011

1 Introduction

There is a substantial body of work applying automata theory to temporal reasoning, with strings (and trees) stretching to infinity to describe non-terminating computation runs (e.g. Emerson Reference Emerson and van Leeuwen1992; Vardi Reference Vardi, Blackburn, Wolter and van Benthem2007). Many natural language statements, however, describe temporally bounded events, including reports in the past tense, such as Pat walked to the post office or An event of such and such happened, that ensure the events have an end (if not a beginning). The question arises: can we employ ordinary finite-state methods (of the sort in, for example, Beesley and Karttunen Reference Beesley and Karttunen2003) to reason about strings that can be assumed finite? The main aim of this paper is to show how we might, and how that may stray from established practices. The focus is not on any particular natural language engineering application, but rather on basic conceptual issues that bear on such applications. These issues revolve around events and situations natural language statements are about—events and situations bounded in ways that merit investigation.

1.1 Linear temporal logic and finite situations

For orientation, we start with linear temporal logic (LTL) over the set 𝕫 of integers and a set P of atomic formulas (e.g. Vardi Reference Vardi, Blackburn, Wolter and van Benthem2007). LTL-formulas are evaluated against relations V ⊆ 𝕫 × P) between 𝕫 and P, with V(t,p) read ‘p is true at V,t’ and written V,t ╠ p

\begin{eqnarray*} V,t \models p \iff V(t,p) \end{eqnarray*}

for t ∈ 𝕫 and p ∈ P. Fixing the evaluation time to 0, we can describe an infinite string of p's through the LTL-formula Gp that asserts V(n,p) for every non-negative integer n

\begin{eqnarray*} V,0 \models {\sf G}p\!\!\!\!\! & \iff & \!\!\!\!\!(\forall n\geq 0)\ V(n,p) \\ & \iff &\!\!\!\!\! \{(n,p)\ | \ n\geq 0\} \subseteq V. \end{eqnarray*}

Negative integers come in to interpret past operators such as previous, from which we can form the LTL-formula previous(q) ∨ Gp that is true at V,0 iff G(p) is or q is true at V,-1

\begin{eqnarray*} V,0 \models \previous(q) \vee {\sf G}p\!\!\!\!\! & \iff &\!\!\!\!\! V(-1,q) \mbox{or} (\forall n\geq 0)\ V(n,p) \\ & \iff &\!\!\!\!\! \{(-1,q)\}\subseteq V \mbox{or} \{(n,p)\ | \ n\geq 0\}\subseteq V \end{eqnarray*}

(for q ∈ P). Assuming P is closed under complementation,Footnote 1 one can, in general, map an LTL-formula ϕ and integer t to a set S [ϕ,t] of relations s ⊆ 𝕫 × P, reducing the truth of ϕ at V,t to some subset of V being in S [ϕ, t]

(1)
\begin{eqnarray} \label{sched} V,t\models \varphi \iff (\exists s\in {\bf S}[\varphi,t]) \ s \subseteq V \ \end{eqnarray}

(e.g. Fernando Reference Fernando2009a). For instance, S[previous(q) ∨ Gp,0] consists of the two relations {(−1,q)} and {(n,p) | n ≥ 0}, each describing a way for previous(q) ∨ Gp to be true at 0. As this example shows, a relation s in S [ϕ, t] may or may not be finite.

Of course, if V were finite, then we can throw out all infinite relations from S([ϕ, t]. Put another way, we can restrict S[ϕ, t] to finite relations by focusing on finite subsets of V (reconstructing V as the union of its finite subsets, as in the reformulation of Büchi acceptance in terms of paths in Fernando Reference Fernando, Hanneforth and Würzner2008b). But we had better be careful about asserting line (1) above for different temporal spans (finite or not), as made clear by the formula Gp saying ‘p now and forever more’ within that span. To establish (1) for spans over only the two times 0 and 1, we put

\begin{eqnarray*} {\bf S}[{\sf G}p,0] = \{\{(0,p),(1,p)\}\} \end{eqnarray*}

but if we add 2 to that span, we would require

\begin{eqnarray*} {\bf S}[{\sf G}p,0] = \{\{(0,p),(1,p), (2,p)\}\}. \end{eqnarray*}

Evidently, varying the temporal spans under consideration (from 𝕫 to its finite segments) renders (1) untenable—at least for ϕ's such as Gp. Such complications beg the question: apart from sidestepping infinite relations s ∈ S[ϕ, t], why should we cut an infinite relation V ⊆ 𝕫 × P down to its finite parts?

At the philosophical end, there is something to be said for grounding semantics in our finite experience, minimizing mysterious abstractions such as possible worlds by working instead with situations that are partial (e.g. Barwise and Perry Reference Barwise and Perry1983). From a more practical natural language processing perspective, it is far from clear that one notion of time will do. Temporal spans vary, as does temporal granularity. Every Monday might mean every Monday in June or every Monday in 2010, and the previous moment might refer to the previous minute or previous second (among many other possibilities). The analysis of calendar expressions in Niemi and Koskenniemi (Reference Niemi, Koskenniemi, Piskorski, Watson and Yli-Jyrä2009) is particularly instructive for our purposes.

1.2 Calendar expressions and snapshots-as-symbols

In Niemi and Koskenniemi (Reference Niemi, Koskenniemi, Piskorski, Watson and Yli-Jyrä2009), temporal span and granularity depend on the calendar expression under consideration. For example, January and March 2008 is interpreted relative to the 12 months of 2008, represented as the string

(2)
\begin{eqnarray} \label{nk08} & \mbox{{\sf [y y2008 [m Jan ]m [m Feb ]m [m Mar ]m $\ldots$ [m Dec ]m ]y}} \end{eqnarray}

of length 39, with 4 bracket symbols ]y, [y, [m and ]m and the 13 symbols y2008, Jan, Feb, (. . .), Dec. The phrase January and March 2008 marks out the months of January and March in (2), leading to

(3)
\begin{eqnarray} \label{nk08M} && \mbox{{\sf [y y2008 $\{i3\ \{i1$ [m Jan ]m $\}i1\ \}i3$ [m Feb ]m $\{i3\ \{i2$ [m Mar ]m $\}i2\ \}i3$}} \ldots \\ \nonumber && \mbox{{\sf [m Dec ]m ]y}} \end{eqnarray}

with six additional symbols {i3, {i2, {i1,}i3,}i2,}i1. We can rewrite (3) as the string

(4)
\begin{eqnarray} \label{m08} && \fbox{y2008,Jan,\(\dagger_3,\dagger_1\)}\fbox{y2008,Feb}\fbox{y2008,Mar,\(\dagger_3, \dagger_2\)}\fbox{y2008,Apr} \cdots \fbox{y2008,Dec} \end{eqnarray}

of length 12 (each box, a symbol) if we rewrite (2) as the string

(5)
\begin{eqnarray} \label{moY} & {\sf \fbox{y2008,Jan}\fbox{y2008,Feb}\fbox{y2008,Mar}\cdots \fbox{y2008,Dec} } \end{eqnarray}

also of length 12. In (4) and (5), a symbol is a subset of some set Φ of fluents (AI-speak for temporal propositions; McCarthy and Hayes Reference McCarthy, Hayes, Meltzer and Michie1969), enclosed by a box (rather than by the more usual curly braces {,}) to suggest a snapshot (or frame in a cartoon strip). As noted in Karttunen (Reference Karttunen2005), we can unpack such boxes, turning (5), for example, into the string

(6)
\begin{eqnarray} \label{moK} & \mbox{\sf [ y2008 Jan ] [ y2008 Feb ] $\cdots$ [ y2008 Dec ] } \end{eqnarray}

of length 48. If Φ is finite and includes neither [ nor ], it is trivial to devise a finite-state transducer mapping strings over the alphabet Pow(Φ) of subsets of Φ to strings over Φ ∪ {[,]}, allowing us to translate regular languages and relations freely between the alphabets Pow(Φ) and Φ ∪ {[,]}. Translating strings in Niemi and Koskenniemi (Reference Niemi, Koskenniemi, Piskorski, Watson and Yli-Jyrä2009) to strings over Pow(Φ) is a more complicated affair and is another day's work. For now, we abstract away from implementation issues for which the strings of Niemi and Koskenniemi (Reference Niemi, Koskenniemi, Piskorski, Watson and Yli-Jyrä2009) were carefully engineered, and work with strings of snapshots.

Strings of snapshots are arguably easier to read because snapshots are ordered chronologically (as in a cartoon or film strip). Indeed, finite subsets of 𝕫 × P for LTL translate straightforwardly into strings over Pow(P ∪ {0}), with, for example,

\begin{eqnarray*} \{(-1,p),(-1,q),(1,p),(3,p)\} & \mbox{translating to} & \fbox{\(p,q\vphantom{0}\)}\fbox{0\vphantom{\(p\)}}\fbox{\(p\vphantom{0}\)} \fbox{\(\vphantom{0p}\)}\fbox{\(p\vphantom{0}\)} \end{eqnarray*}

(suggesting we equate Φ with P ∪ {0}). That said, we should be careful not to fix the notion of time (say, to 𝕫) if we are to accommodate different granularities. That is, the brackets [ and ] in (6) should be understood as having indeterminate granularity (in contrast to [m and ]m in (2) and (3)). Moreover, we may compress (4) to

(7)
\begin{eqnarray} \label{m08E} & \fbox{y2008,Jan,\(\dagger_3\)}\fbox{y2008,Mar,\(\dagger_3\)} \end{eqnarray}

just as Niemi and Koskenniemi compress (3) to

\begin{eqnarray*} & \mbox{{\sf [y y2008 $\{i3$ [m Jan ]m $\}i3$ $\{i3$ [m Mar ]m $\}i3$ ]y}} \end{eqnarray*}

with unmarked calendar periods removed (Niemi and Koskenniemi Reference Niemi, Koskenniemi, Piskorski, Watson and Yli-Jyrä2009: 129). Unlike the timelines depicted by (4) and (5), there are gaps between the boxes in (7) that are familiar to conceptions of time based on discrete transitions, be they the input/output pairs of programs in dynamic logic (Harel, Kozen and Tiuryn Reference Harel, Kozen and Tiuryn2000) or strings of length ≥3 (with intermediate states) for temporal logic. In any case, it is of interest to isolate (7) from (4), or even better, (7)'s unmarked variant

(8)
\begin{eqnarray} \label{m08U} & \fbox{y2008,Jan}\fbox{y2008,Mar} \end{eqnarray}

from (4)'s

(9)
\begin{eqnarray} & {\sf \fbox{y2008,Jan}\fbox{y2008,Feb}\fbox{y2008,Mar}\cdots \fbox{y2008,Dec} } \end{eqnarray}

inasmuch as the mapping (9) ↦ (8) constitutes, in the words of Niemi and Koskenniemi (Reference Niemi, Koskenniemi, Piskorski, Watson and Yli-Jyrä2009), a ‘disambiguated intensional meaning’ of January and March 2008.

1.3 Carnap–Montague intensions and partiality

The (Carnap–Montague) intension of an expression is a function from indices to extensions (or denotations). For the expression January and March 2008 above, we can view the string (9) as an index, and (8) as an extension. Since Frege, it has been customary to identify the extension of a sentence (or statement) ϕ with one of two truth values, say True and False, essentially reducing the intension 𝓘[ϕ] of ϕ to the set of indices that 𝓘[ϕ] maps to True. For LTL, an index is a pair V, t where V ⊆ 𝕫 × P and t ∈ 𝕫, and

\begin{eqnarray*} \cI[\varphi](V,t) = \mbox{True} & \TFbd{\iff} & V,t\models \varphi. \end{eqnarray*}

Now, the main idea behind the present work is to reconceptualize

  1. (i) an index as a string over the alphabet Pow(Φ) built from a set Φ of fluents including now ∈ Φ) through which we can encode, for instance, the pair

    \begin{eqnarray*} \{(-1,p),(-1,q),(1,p),(4,r)\},\ 2 \end{eqnarray*}
    as the string
    \begin{eqnarray*} \fbox{\(p,q\vphantom{0}\)}\fbox{0\vphantom{\(p\)}}\fbox{\(p\vphantom{0}\)} \fbox{\(\TFnow\vphantom{0p}\)}\fbox{\(\vphantom{0p}\)} \fbox{\(r\vphantom{0p}\)} \end{eqnarray*}
    and

  2. (ii) an extension of a sentence ϕ as a set of strings over Pow(Φ), rather than True or False

so that the intension 𝓘[ϕ] of ϕ maps a string s ∈ Pow(Φ)* to a set 𝓘[ϕ](s) ⊆ Pow(Φ)* of strings that make ϕ true at s inasmuch as

(10)
\begin{eqnarray} \label{tru} \varphi \mbox{is true at} \sss \TFbd{\iff} \cI[\varphi](\sss)\neq\emptyset. \end{eqnarray}

If we relax the requirement that an intension be a function and require simply that it be a binary relation between indices and extensions, then we can formulate indices and extensions alike as strings over Pow(Φ), identifying the intension of ϕ with the binary relation

\begin{eqnarray*} \cR[\varphi] \TFbd{=} \{(\sss,\sss')\in \mbox{domain}(\cI[\varphi]) \times \TFPow(\Phi)^\ast \ | \ \sss'\in \cI[\varphi](\sss)\} \end{eqnarray*}

on Pow(Φ)*. A string in Pow(Φ)* can be understood as a situation in the sense of Barwise and Perry (Reference Barwise and Perry1983) (as opposed to that in McCarthy and Hayes Reference McCarthy, Hayes, Meltzer and Michie1969). In case 𝓘[ϕ](s) consists of exactly one situation s', we can say s' is the situation described by ϕ at s, linking the event time in Reichenbach (Reference Reichenbach1947) to the temporal span of s' (in contrast to the time now marks out in the index s). Indeed, events in Davidsonian semantics exemplify situations as truthmakers (Davidson Reference Davidson and Rescher1967; Mulligan, Simons and Smith Reference Mulligan, Simons and Smith1984). The domain of 𝓡[ϕ] consists, under (10), of the indices at which ϕ is true, qualifying as the truth set 𝓣[ϕ] of ϕ

\begin{eqnarray*} \cT[\varphi] \TFbd{=} \{\sss\in \TFPow(\Phi)^\ast\ | \ (\exists \sss')\ \sss\ \cR[\varphi]\ \sss'\}. \end{eqnarray*}

The image of 𝓡[ϕ] consists of situations that ϕ is about, making it the about set of ϕ, which we write 𝒜[ϕ]

\begin{eqnarray*} \cA[\varphi] \TFbd{=} \{\sss'\in \TFPow(\Phi)^\ast\ | \ (\exists \sss)\ \sss\ \cR[\varphi]\ \sss'\} \end{eqnarray*}

(see Table 1, Fernando Reference Fernando2009b).

Table 1.

Basic notions from an intension function 𝓘[ϕ].

Setting aside the problem that aboutness need not be grounded in truth, let us explore the intuition that

(11)
\begin{eqnarray} \label{about} \sss\ \cR[\varphi]\ \sss' & \mbox{can be read:} & \varphi \mbox{is about $\sss'$ in} \sss. \end{eqnarray}

It is certainly plausible to assume that s 𝓡[ϕ] s' implies s' ⊑ s, for some ‘in’ relation ⊑ on strings over Pow(Φ). One way to formalize (11) then is to combine the about set 𝓐[ϕ] with ⊑ for the biconditional

(12)
\begin{eqnarray} \label{abs} \sss\ \cR[\varphi]\ \sss' & \iff& \sss'\in \cA[\varphi] \mbox{and} \sss'\sqsubseteq \sss . \end{eqnarray}

An immediate consequence of (12) is that for transitive relations ⊑, truth is persistent in that 𝓣(ϕ) is closed under ⊑

(13)
\begin{eqnarray} \label{per} \sss_1\in \cT[\varphi] \mbox{and} \sss_1 \sqsubseteq \sss_2 & \implies & \sss_2 \in \cT[\varphi] \end{eqnarray}

for all s1,s2 ∈ Pow(Φ)*. While (13) may hold for many sentences ϕ, there are well-known counter-examples to it, including the LTL-formula Gp in Section 1.1. Recall that the biconditional

(14)
\begin{eqnarray} V,t\models \varphi \iff (\exists s\in {\bf S}[\varphi,t]) \ s \subseteq V \ \end{eqnarray}

becomes problematic when we work with bounded temporal spans short of 𝕫 (replacing, as it were, V with its finite subsets). To link this discussion up with (12), some notation is helpful. Given a finite subset s of 𝕫 × P and an integer t, let us write str(s,t) for the shortest string over Pow(P ∪ {0, now}) encoding the pair s,t. For instance,

\begin{eqnarray*} \TFstr(\{(-1,p),(-1,q),(1,p),(4,r)\},\ 2) = \fbox{\(p,q\vphantom{0}\)}\fbox{0\vphantom{\(p\)}}\fbox{\(p\vphantom{0}\)} \fbox{\(\TFnow\vphantom{0p}\)}\fbox{\(\vphantom{0p}\)} \fbox{\(r\vphantom{0p}\)}. \end{eqnarray*}

The notions of ‘in’ ⊑ then becomes essentially set inclusion ⊆

\begin{eqnarray*} \TFstr(s,t) \sqsubseteq \TFstr(s',t') \iff t=t'\mbox{and} s\subseteq s' \end{eqnarray*}

while ‘about’ 𝓐[ϕ] corresponds to t∈𝕫S[ϕ, t]

\begin{eqnarray*} \cA[\varphi] = \{\TFstr(s,t) \ | \ t\in𝕫 \mbox{and} s\in {\bf S}[\varphi,t]\}. \end{eqnarray*}

Now the difficulty (14) poses for Gp when V is replaced by its finite fragments s' suggests that the best we can salvage from (14) is to step from a set S[ϕ, t] of relations between 𝕫 and P to some suitable binary relation R[ϕ, t] between such relations, and weaken (14) to

(15)
\begin{eqnarray} \label{tRue} s',t\models \varphi \iff (\exists s)\ s'\ {\bf R}[\varphi,t]\ s. \end{eqnarray}

That is, if

\begin{eqnarray*} \cR[\varphi] = \{(\TFstr(s,t), \TFstr(s',t)) \ | \ t\in𝕫 \mbox{and} s\ {\bf R}[\varphi,t]\ s'\}\ \end{eqnarray*}

then (15) equates the truth set 𝓣[ϕ] with the domain of 𝓡[ϕ]. But if we are to read s 𝓡[ϕ] s' as

(16)
\begin{eqnarray} \label{abo} \varphi \mbox{is about $\sss'$ in} \sss \end{eqnarray}

then we had better beware that

(17)
\begin{eqnarray} \label{abo0} \sss'\in \cA[\varphi] &\mbox{and} & \sss'\sqsubseteq \sss \end{eqnarray}

falls short of (16) for sentences ϕ such as Gp. Picking out the sentences where (16) reduces to (17), let us define ϕ to be absolute if

(18)
\begin{eqnarray} \sss\ \cR[\varphi]\ \sss' \iff \sss'\in \cA[\varphi] \mbox{and} \sss'\sqsubseteq \sss \end{eqnarray}

for all s,s' ∈ Pow(Φ)*. The LTL-formulas p and previous(q) are absolute; Gp is not.

Whether or not ϕ is absolute, it is useful for 𝓡[ϕ] to be a regular relation because it gives us a computational handle not only on its image, the about set 𝓐[ϕ], but also on its domain, the truth set 𝓣(ϕ). Entailment ├ between sentences is often relativized to constraints C, which we can identify with a set of strings (following, for example, Beesley and Karttunen Reference Beesley and Karttunen2003) to define

\begin{eqnarray*} \varphi\proves_C \psi \!\!\!\!\! &\TFbd{\iff}& \!\!\!\!\! (\forall \sss\in C)\ \varphi\mbox{is true at} \sss \implies \psi\mbox{is true at} \sss\\ &\iff&\!\!\!\!\! C\cap \cT[\varphi] \ \subseteq \ \cT[\psi]. \end{eqnarray*}

If 𝒯[ϕ], 𝒯[ψ] and C are all regular languages, then ├C above is decidable (since inclusion between regular languages is). Note that the strings in 𝓣[ϕ] are finite, whereas the relations V⊆ 𝕫 × P in LTL-semantics can be infinite, collectively inducing the entailments

\begin{eqnarray*} \varphi \proves^{{\rm LTL}} \psi \TFbd{\iff} (\forall V\subseteq {\ZZ}\times P)\,(\forall t\in{\ZZ}) \ V,t\models \varphi \implies V,t\models \psi\ \end{eqnarray*}

1.4 Claims and some finite-state matters

The bounded entailments ├C provide approximations of ├LTL that we take up in Section 3. But far from providing a new, improved way of calculating ├LTL (which we do not), the point of introducing relations 𝓡[ϕ] is to reason beyond ├LTL,

  1. (a1) breaking free from the tyranny of the clock 𝕫 built into the semantics behind ├LTL

and

  1. (a2) bringing out the about sets 𝓐[ϕ] that are at best implicit in that semantics.

The ‘tyranny of the clock 𝕫’ mentioned in (a1) is twofold: its span is infinite (two ways), and its ticks (grain) are fixed by the successor (plus-1) relation (in 𝕫). The focus below is on bounding span, although a few words about grain are offered at the conclusion on which I hope to expand elsewhere.

As for (a2), the proposed relational semantics 𝓡[ϕ] consists not only of the indices in 𝓣(ϕ) that shape ϕ ├C ψ, but also of denotations in 𝓐[ϕ], exemplified by events (e.g. Fernando Reference Fernando2009b). It is notable that Hans Kamp, famous in temporal logic for since and until, leaves temporal logic out of Discourse Representation Theory (Kamp and Reyle Reference Kamp and Reyle1993: 492) and works instead with events. As useful as it has proved in computer science, LTL is an artificial language, unfit for linguistic analyses that posit, for instance, two forms of until, dependent on the (a)telicity of event descriptions, featuring presuppositional as well as assertional dimensions (e.g. Karttunen Reference Karttunen1974; Condoravdi Reference Condoravdi, Hanson and Inkelas2009). Introducing relations 𝓡[ϕ] moves us, I claim, closer to an account of events (as denotations) and presuppositions (via indices). This is not a small claim, and I shall confine myself here to events as denotations. Analyzing presuppositions as requirements on indices calls for (in my view) adjustments to the definitions of 𝓡[ϕ] given below.

Presuppositions and telicity aside, let us consider the past tense, and ask if the LTL clause

\begin{eqnarray*} V,t\models {\sf P}\varphi \TFbd{\iff} (\exists t'\leq t)\ V,t'\models \varphi \end{eqnarray*}

supports a reading of Pϕ as ‘ϕ in the present or in the past’? It is plausible enough in case ϕ is an atomic formula p for which V(t,p) says there is a V-situation of type p with time t. But suppose ϕ were constructed from the connective until, under the LTL clause

\begin{eqnarray*} V,t\models \psi\ \TFuntil\ \chi \!\!\!\!\!& \TFbd{\iff} & \!\!\!\!\! (\exists t'\geq t)\ V,t'\models \chi \mbox{and} \\ & & \hspace{.55in} \mbox{whenever} t\leq t''< t', \ V,t''\models \psi \end{eqnarray*}

(such as it isFootnote 2). It is natural to assume that part of a V-situation of type ψ until p is a V-situation of type p. But for V ° = {(0,q), (1,q),(2,q),(3,p)}, we have

\begin{eqnarray*} V_\circ,1 \models {\sf P}(q\ \TFuntil\ p) \end{eqnarray*}

even though every V °-situation of type q until p stretches to 3, which is not in the past of 1. In general, for non-atomic ϕ, one cannot conclude from V,t' ⊧ ϕ and t' < t that there is a V-situation of type ϕ in the past of t. To report ϕ in the past tense at speech time t in V, what we require is not some t' < t such that V,t' ⊧ ϕ but a truthmaker for ϕ in the past of t.Footnote 3 That is, it is not so much the domain 𝓣[ϕ] of 𝓡[ϕ] that is relevant, but rather the image 𝓐[ϕ] of 𝓡[ϕ] and the ‘in’ relation ⊑.

The next section fleshes out relations 𝓡[ϕ] and ⊑ in finite-state terms. Under the conventions adopted in, for example, Regular Model Checking (Bouajjani et al. Reference Bouajjani, Jonsson, Nilsson and Touili2000), regular relations can hold only between strings of the same length. But for ⊑ (for instance) to be regular, we drop this requirement, and follow Beesley and Karttunen (Reference Beesley and Karttunen2003) in permitting a finite-state transducer to make componentwise ε-moves (where ε is the null/empty string). A notable difference between Bouajjani et al. (Reference Bouajjani, Jonsson, Nilsson and Touili2000) and Beesley and Karttunen (Reference Beesley and Karttunen2003) is that regular relations are closed under intersection in the former but not in the latter. What is important for our purposes, however, is that the basic notions summarized in Table 2 are regular. A factor of s is a string s' such that s = us's for some strings u and v. The relation has-factor defined by

Table 2.

Some regular notions given a regular language L and relation R.

\begin{eqnarray*} \sss\ \hfac\ \sss' \TFbd{\iff} (\exists \uuu, \vvv) \ \sss= \uuu\sss'\vvv \end{eqnarray*}

is computed by the finite-state transducer with three states 0,1,2, all final (accepting), 0 initial, with loops

\begin{eqnarray*} 0\TFtr{\alpha:\epsilon} 0 \ \mbox{and} \ 2\TFtr{\alpha:\epsilon} 2 \quad \mbox{for every symbol} \alpha \end{eqnarray*}

plus transitions

(19)
\begin{eqnarray} \label{trans} 0\TFtr{\alpha:\alpha} 1 \TFtr{\alpha:\alpha} 1\TFtr{\alpha:\alpha} 2 \quad \mbox{for every symbol} \alpha. \end{eqnarray}

Given a finite-state transducer for R with transitions →R and a finite automaton for L with transitions →L, we can form a finite-state transducer for the (right) L-restriction R L of R defined by

\begin{eqnarray*} R_L \TFbd{=} \{(\sss,\sss')\in R\ | \ \sss'\in L\} \end{eqnarray*}

by collecting the transitions

(20)
\begin{eqnarray} \label{trRe} (q,q') \TFtr{\alpha:\alpha'} (r,r') \quad \mbox{for}\quad q \stackrel{\alpha:\alpha'}{\to}_R r \mbox{and} (q' \stackrel{\alpha'}{\to}_L r' \mbox{or} (\alpha'=\epsilon\mbox{and} q'=r')) \end{eqnarray}

(as in the usual construction for the intersection of regular languages, but with ε-moves). The domain of R L is the Peirce product 〈R〉 L of R with L Footnote 4

\begin{eqnarray*} \tuple{R}L \TFbd{=} \{\sss\ | \ (\exists \sss')\ \sss \ R_L\ \sss'\}, \end{eqnarray*}

for which we existentially quantify α' out from (20) for

\begin{eqnarray*} (q,q') \TFtr{\alpha} (r,r') \quad \mbox{whenever}\quad (\exists \alpha')\ q \stackrel{\alpha:\alpha'}{\to}_R r \mbox{and} (q' \stackrel{\alpha'}{\to}_L r' \mbox{or} (\alpha'=\epsilon\mbox{and} q'=r')). \end{eqnarray*}

And as regular languages are closed under Boolean operations, including complementation $\(\overline{L} \TFbd{=} \Sigma^\ast - L\) $ over the alphabet Σ, we can form the dual [R]L of the Peirce product 〈R〉L

\begin{eqnarray*} {[R]}L\!\!\!\!\! & \TFbd{=} &\!\!\!\! \overline{\tuple{R}\overline{L}}\\ & = &\!\!\!\! \{\sss\in\Sigma^\ast\ | \ (\forall \sss'\mbox{such that} \sss\ R\ \sss')\ \sss'\in L\} \end{eqnarray*}

just as ∀ is the dual of ∃.

In the remainder of this paper, strings are formed from the alphabet Σ = Pow(Φ), under the assumption that Φ is finite, so that there are only finitely many subsets of Φ (i.e. symbols) which we write α, α', β), etc. That is, a string s∈ Pow(Φ)* is a sequence of the form α1. . .αn, while a symbol α is a box of fluents (from Φ). Largely a matter of convenience, this choice of alphabet provides a level of abstraction that simplifies many of the constructions below.

2 Relations 𝓡[ϕ] for some absolute formulas ϕ

This section starts with a simple generalization of set inclusion to strings over the alphabet Pow(Φ), which is then used to formulate constraints such as

\begin{eqnarray*} \fbox{\(\varphi\wedge\psi\)} \Rightarrow \fbox{\(\varphi,\psi\)} \end{eqnarray*}

picking out strings that contain ϕ ∧ ψ only if they contain ϕ and ψ in the same box. Some refinements are then made to capture the ‘in’ relation ⊑ and define 𝓡[ϕ] for various absolute sentences ϕ.

2.1 Subsumption and constraints

Checking set inclusion ⊇ componentwise between strings from Pow(Φ)* of the same length, let

\begin{eqnarray*} \alpha_1\cdots\alpha_n \ \unrhd\ \alpha'_1\cdots\alpha'_m \TFbd{\iff} n=m \mbox{and} \alpha_i\supseteq \alpha'_i \mbox{for} 1\leq i\leq n \end{eqnarray*}

for all symbols αi,α'i ⊆ Φ). (Exactly what is in Φ does not matter just now, as long as Φ is finite.) In Fernando (Reference Fernando2004), s ⊵ s' is pronounced: s subsumes s'. The relation is computed by the finite-state transducer with a single state 0, both initial and final, and transitions

\begin{eqnarray*} 0 \TFtr{\alpha:\alpha'} 0 \quad \mbox{for}\quad \alpha'\subseteq\alpha\subseteq\Phi. \end{eqnarray*}

Next, given a language L over Pow(Φ), we let s ⊵ L mean s belongs to the Peirce product 〈⊵〉L (read: s subsumes L)

\begin{eqnarray*} \sss\unrhd L\!\!\!\!\! & \TFbd{\iff} &\!\!\!\!\! \sss\in\tuple{\unrhd}L \\ & \iff &\!\!\!\!\! (\exists \sss'\in L)\ \sss\unrhd \sss'. \end{eqnarray*}

Then, given another language L' over Pow(Φ), let L ⇒ L' be the set of strings s such that every factor of s that subsumes L also subsumes L'

\begin{eqnarray*} L\Rightarrow L' \TFbd{=} \{\sss\in \TFPow(\Phi)^\ast | \mbox{for every factor $\sss'$ of} \sss, \sss'\unrhd L \mbox{implies} \sss'\unrhd L'\}. \end{eqnarray*}

Collecting the factors of s that subsume L in the 〈⊵〉 L-restriction of has-factor

\begin{eqnarray*} \sss\ \hfac_{\tuple{\unrhd}L}\ \sss' \!\!\!\!\! &\TFbd{\iff}& \!\!\!\!\! \sss\ \hfac\ \sss' \mbox{and} \sss'\in\tuple{\unrhd} L \\ & \iff & \!\!\!\!\! \sss\ \hfac\ \sss' \mbox{and} \sss'&#x22B5; L, \end{eqnarray*}

it follows that

\begin{eqnarray*} L\Ra L' = [\hfac_{\tuple{\unrhd}L}] \tuple{\unrhd}L'. \end{eqnarray*}

From the regularity of the constructs in Table 2, we can conclude that L ⇒ L' is a regular language if L and L' are. Indeed,

\begin{eqnarray*} L\Rightarrow L' = \overline{\TFPow(\Phi)^\ast \ (\tuple{\unrhd}L \cap \overline{\tuple{\unrhd}L'})\ \TFPow(\Phi)^\ast}. \end{eqnarray*}

Among the constraints we can formulate with ⇒ are

\begin{eqnarray*} \fbox{\(\varphi\vee\psi\)} \Rightarrow \fbox{\(\varphi\vphantom{\psi}\)} \ | \ \fbox{\(\psi\)}\ \end{eqnarray*}

picking out strings that contain ϕ ∨ ψ only if they contain ϕ or ψ in the same box,

\begin{eqnarray*} \ \fbox{\(\vphantom{\overline{\varphi}}\)} \Ra \fbox{\(\varphi\vphantom{\overline{\varphi}}\)} \ | \ \fbox{\(\overline{\varphi}\)} \end{eqnarray*}

requiring either ϕ or its negation ϕ to be in every box. and

\begin{eqnarray*} \fbox{\(\varphi,\overline{\varphi}\)} \Ra \emptyset \end{eqnarray*}

banning ϕ and ϕ from occurring in the same box.

We can also form

\begin{eqnarray*} \fbox{\TFnext(\(\varphi\))} \fbox{\(\vphantom{\TFnext(\varphi)}\)} \Ra \fbox{\(\vphantom{\TFnext(\varphi)}\)} \fbox{\(\varphi\vphantom{\TFnext(\varphi)}\)} \end{eqnarray*}

to put ϕ at every box succeeding one containing next(ϕ), in line with the LTL clause

\begin{eqnarray*} V,t\models \TFnext(\varphi) \TFbd{\iff} V,t+1\models \varphi. \end{eqnarray*}

But to require that there be a box after every box containing next(ϕ), we form

\begin{eqnarray*} \fbox{\(\TFnext(\varphi)\)} \stackrel{{\sf a}}{\Rightarrow} \fbox{\(\varphi\vphantom{\TFnext()}\)}, \end{eqnarray*}

where $\(L\stackrel{{\sf a}}{\Rightarrow} L'\)$ is pronounced ‘L’ after every L' and

\begin{eqnarray*} L\stackrel{{\sf a}}{\Rightarrow} L'\!\!\!\!\! & \TFbd{=} & \!\!\!\!\! \{\sss\in\TFPow(\Phi)^\ast\ | \ \mbox{after every factor of $s$ that subsumes} L \\ && \hspace{.95in} \mbox{is a string that subsumes} L'\}. \end{eqnarray*}

Defining

\begin{eqnarray*} \sss\mbox{{\it after\/}}^L\ \sss' \TFbd{\iff} (\exists \uuu\unrhd \square^\ast L) \ \sss=\uuu\sss', \end{eqnarray*}

we get

\begin{eqnarray*} L\stackrel{{\sf a}}{\Rightarrow} L' = [\mbox{{\it after\/}}^L]\ \tuple{\unrhd} (L'\square^\ast). \end{eqnarray*}

It is not difficult to convert a finite automaton for L into a finite-state transducer for after L. Hence, $\(L\stackrel{{\sf a}}{\Rightarrow} L'\)$ is regular if L and L' are. In fact,

\begin{eqnarray*} L\stackrel{{\sf a}}{\Rightarrow} L' = \overline{\tuple{\unrhd}(\square^\ast L)\ \overline{\tuple{\unrhd}(L'\square^\ast)}}. \end{eqnarray*}

Modulo subsumption $\(\unrhd\), \(L \stackrel{{\sf a}}{\Rightarrow} L'\)$ is one form of Koskenniemi's restrictions (Beesley and Karttunen Reference Beesley and Karttunen2003), a second one being $\(L\stackrel{{\sf b}}{\Rightarrow} L'\)$, read ‘L’ before every L,' defined by

\begin{eqnarray*} L\stackrel{{\sf b}}{\Rightarrow} L' \TFbd{=} [\mbox{{\it before\/}}^L]\ \tuple{\unrhd}(\square^\ast L'), \end{eqnarray*}

where

\begin{eqnarray*} \sss\mbox{{\it before\/}}^L\ \sss' \TFbd{\iff} (\exists \vvv\unrhd L\square^\ast)\ \sss=\sss'\vvv . \end{eqnarray*}

As with ⇒ and $\(\stackrel{{\sf a}}{\Rightarrow}\), \(L\stackrel{{\sf b}}{\Rightarrow} L'\)$ is regular if L and L' are, with

\begin{eqnarray*} L\stackrel{{\sf b}}{\Rightarrow} L' = \overline{ \overline{\tuple{\unrhd}(\square^\ast L')} \ \tuple{\unrhd}(L \square^\ast)}. \end{eqnarray*}

We can also strengthen $\(\fbox{\)\vphantom{\TFprev(\varphi)}\(} \fbox{\TFprev(\)\varphi\()}\ \! &#x21D2;\ \fbox{\)\varphi\vphantom{\TFprev(\varphi)}\(} \fbox{\)\vphantom{\TFprev(\varphi)}\(}\)$ to

\begin{eqnarray*} \fbox{\TFprev(\(\varphi\))} \,\stackrel{{\sf b}}{\Rightarrow}\, \fbox{\(\varphi\)} \ \end{eqnarray*}

for the LTL clause

\begin{eqnarray*} V,t\models \TFprev(\varphi) \TFbd{\iff} V,t-1\models \varphi. \end{eqnarray*}

Both ⇒ and $\(\stackrel{{\sf a}}{\Rightarrow}\)$ are useful to analyze ϕ until ψ through auxiliary formulas ϕ ntil ψ

\begin{eqnarray*} \fbox{\(\varphi\ \TFuntil\ \psi\)} \Rightarrow \fbox{\(\psi\)} \ | \ \fbox{\(\varphi,\ \varphi\ \TFntil\ \psi\)} \end{eqnarray*}

with

\begin{eqnarray*} \fbox{\(\varphi\ \TFntil\ \psi\)} \stackrel{{\sf a}}{\Rightarrow} \fbox{\(\vphantom{\psi}\varphi\)}^\ast \fbox{\(\psi\)}. \end{eqnarray*}

(Thus, if p and q are atomic formulas, we can picture p until q roughly as $\(\fbox{\)p\(}^\ast\fbox{\)q\(}\).$) Similarly, for since under the LTL clause

\begin{eqnarray*} V,t\models \varphi\ \TFsince\ \psi\!\!\!\!\! & \TFbd{\iff} & \!\!\!\!\! (\exists t'\leq t) (V,t'\models \psi\mbox{and} \\ & & \hspace{.5in} \mbox{whenever} t'< t'' \leq t, \ V,t''\models \varphi) \end{eqnarray*}

we apply $\(\stackrel{{\sf b}}{\Rightarrow}\)$ and auxiliary formulas ϕ sinc ψ

\begin{eqnarray*} \fbox{\(\varphi\ \TFsince\ \psi\)} \!\!\!\!& \Rightarrow & \!\!\!\! \fbox{\(\psi\)} \ | \ \fbox{\(\varphi,\ \varphi\ \TFsinc\ \psi\)}\\ \fbox{\(\varphi\ \TFsinc\ \psi\)} \!\!\!\! & \stackrel{{\sf b}}{\Rightarrow} & \!\!\!\! \fbox{\(\psi\)}\fbox{\(\varphi\vphantom{\psi}\)}^\ast. \end{eqnarray*}

If we fix a tautology ┬ with the vacuous constraint

\begin{eqnarray*} \fbox{\(\top\)} \Rightarrow \fbox{\(\vphantom{\top}\)} \end{eqnarray*}

then the Priorean past Pϕ can be understood as an abbreviation of ┬ since ϕ, and its future counterpart Fϕ as ┬ until ϕ.

2.2 Unpadding for information content

Although the relation ⊵ is just right for formulating constraints, it is convenient to weaken it slightly to compare strings of different lengths. A candidate for the converse of the ‘in’ relation ⊑ from Section 1.3 satisfying

\begin{eqnarray*} \TFstr(s,t) \sqsupseteq \TFstr(s',t') \iff t=t' \mbox{and}s\supseteq s' \end{eqnarray*}

for all finite s,s'⊆𝕫 × P and t,t' ∈ 𝕫 is the relation ⊒° composing has-factor with ⊵

\begin{eqnarray*} \sss\ \sqsupseteq_\circ\ \sss'\!\!\!\!\! & \TFbd{\iff} & \!\!\!\!\! \sss\ \hfac;\unrhd\ \sss' \\ & \iff & \!\!\!\!\! (\exists \uuu, \sss'',\vvv) \ \sss= \uuu\sss''\vvv \mbox{and} \sss'' \unrhd \sss'. \end{eqnarray*}

A finite-state transducer for ⊒° can be built from the one described in Section 1.4 above for has-factor by generalizing the transitions in line (19) to

\begin{eqnarray*} 0\TFtr{\alpha:\alpha'} 1 \TFtr{\alpha:\alpha'} 1\TFtr{\alpha:\alpha'} 2 \quad \mbox{for} \alpha'\subseteq\alpha\subseteq\Phi. \end{eqnarray*}

The relation ⊒° has the defect, however, that s ⊒ s' may fail to hold because of empty boxes in s' — e.g. $\(\fbox{\TFnow}\not\sqsupseteq_\circ \fbox{\vphantom{\TFnow}} \fbox{\TFnow}\).$ Accordingly, we unpad a string sinPow(Φ)* by deleting all initial and final □'s

\begin{eqnarray*} \unpad(\sss) \TFbd{=} \left\{\begin{array}{@{}ll@{}} \sss & \mbox{if $\sss$ neither begins nor ends with} \square \\ \unpad(\sss') & \mbox{if} \sss=\square \sss' \mbox{or else if} \sss=\sss'\square \end{array}\right. \end{eqnarray*}

so that for example, $\(\unpad(\fbox{\)\vphantom{p}\(} \fbox{\)p\(}\fbox{\)\vphantom{p}\(} \fbox{\TFnow\)\vphantom{p}\(} \fbox{\)\vphantom{p}\(} \fbox{\)\vphantom{p}\(}) = \fbox{\)p\(}\fbox{\)\vphantom{p}\(} \fbox{\TFnow\)\vphantom{p}\(}\).$ Next, we say s and s' are unpad-equivalent if their unpadding is identical

\begin{eqnarray*} \sss \approx \sss' \TFbd{\iff} \unpad(\sss) = \unpad(\sss') \end{eqnarray*}

and say a string sweakly subsumes s', written s⊒ s', if some string unpad-equivalent to s subsumes some string unpad-equivalent to s'

\begin{eqnarray*} \sss \unrhdSQ \sss' \TFbd{\iff} (\exists \sss_\circ\approx \sss)(\exists \sss'_\circ\approx \sss') \ \sss_\circ\unrhd \sss'_\circ. \end{eqnarray*}

The relations unpad and ≈ are regular, and as

\begin{eqnarray*} \sss\unrhdSQ \sss' \!\!\!\!\!& \iff &\!\!\!\!\! (\exists \sss'_\circ\approx\sss') \ \sss\unrhd \sss'_\circ\\ & \iff & \!\!\!\!\! \sss \sqsupseteq_\circ \unpad(\sss') \end{eqnarray*}

we can turn the finite-state transducer for ⊒° above into one for ⊒ by adding the loops

\begin{eqnarray*} 0\TFtr{\epsilon:\square} 0 & \mbox{and} & 2\TFtr{\epsilon:\square} 2. \end{eqnarray*}

Of course, if we arrange that s' = unpad(s') for strings s' that we put to the right of ⊒, we can make do with ⊒° instead of ⊒.

Table 3.

Comparing information content

It is natural to think of strings in a language as possibilities in the same way that worlds in a proposition are under possible worlds semantics (or models of a sentence are in model-theoretic semantics). We lift ⊒ to languages L,L′ through the Peirce product

\begin{eqnarray*} L\unrhdSQ L'\!\!\!\!\! & \TFbd{\iff} &\!\!\!\!\! L\subseteq \tuple{\unrhdSQ}L' \\ & \iff &\!\!\!\!\! (\forall \sss\in L)(\exists \sss'\in L')\ \sss\unrhdSQ \sss' \end{eqnarray*}

paralleling the definition in possible worlds semantics that a proposition A entails a proposition A′ if A ⊆ A′. To weed out spurious possibilities, it is useful to bring in a language C to intersect with 〈⊒〉L for

\begin{eqnarray*} C[L] \TFbd{=} C\cap\tuple{\unrhdSQ}L \ \end{eqnarray*}

and then beef up L ⊒ L′ to an entailment

\begin{eqnarray*} L \proves_C L' \!\!\!\!\! & \TFbd{\iff} & \!\!\!\!\! C[L]\ \unrhdSQ\ L' \\ & \iff & \!\!\!\!\! C\cap\tuple{\unrhdSQ}L\ \subseteq\ \tuple{\unrhdSQ}L'. \end{eqnarray*}

Clearly, L ├CL′ whenever L ⊒ L′. The introduction of C allows us not only to enlarge a string in L to one in 〈⊒〉L, but also to restrict attention to strings meeting the membership conditions for C

\begin{eqnarray*} L \proves_C L' \iff (\forall \sss\in C)\ \sss\unrhdSQ L \mbox{implies} \sss\unrhdSQ L'. \end{eqnarray*}

These membership conditions can be viewed as constraints (to satisfy), as we see next.

2.3 Some absolute formulas

A sentence ϕ is absolute if its description relation 𝓡[ϕ] is the 𝓐[ϕ]-restriction of ⊒, making its truth set 𝓣(ϕ) the Peirce product 〈⊒〉𝒜[ϕ]. We now flesh out 𝓐[ϕ] for certain absolute LTL-formulas ϕ—in particular, those belonging to the set P + of formulas that can be formed from a set P of atomic formulas using the connectives ∧, ∨, next, previous, until, ntil, since, sinc. We start with constraints 𝓒(ϕ) for ϕ ∈ P +, setting

\begin{eqnarray*} \cC(\varphi\wedge\psi)\!\!\! & \TFbd{=} &\!\!\! \cC(\varphi) \cap \cC(\psi) \cap (\fbox{\(\varphi\wedge\psi\)}\Rightarrow\fbox{\(\varphi,\psi\)}) \\ \cC(\varphi\vee\psi) \!\!\!& \TFbd{=} & \!\!\! \cC(\varphi) \cap \cC(\psi) \cap (\fbox{\(\varphi\vee\psi\)}\Rightarrow\fbox{\(\varphi\vphantom{\psi}\)}|\fbox{\(\psi\)}) \\ \cC(\TFnext(\varphi)) \!\!\!& \TFbd{=} &\!\!\! \cC(\varphi) \cap (\fbox{\(\TFnext(\varphi)\)}\stackrel{{\sf a}}{\Rightarrow} \fbox{\(\varphi\vphantom{\TFnext()}\)}) \\ \cC(\TFprev(\varphi)) \!\!\!& \TFbd{=} & \!\!\! \cC(\varphi) \cap (\fbox{\(\TFprev(\varphi)\)}\stackrel{{\sf b}}{\Rightarrow} \fbox{\(\varphi\vphantom{\TFprev()}\)}) \\ \cC(\varphi\ \TFuntil\ \psi) \!\!\!& \TFbd{=} &\!\!\! \cC(\varphi\ \TFntil\ \psi) \cap (\fbox{\(\varphi\ \TFuntil\ \psi\)}\Rightarrow\fbox{\(\psi\)} | \fbox{\(\varphi,\ \varphi\ \TFntil\ \psi\)} ) \\ \cC(\varphi\ \TFntil\ \psi) \!\!\!& \TFbd{=} &\!\!\! \cC(\varphi) \cap \cC(\psi) \cap (\fbox{\(\varphi\ \TFntil\ \psi\)}\stackrel{{\sf a}}\Rightarrow \fbox{\(\varphi\vphantom{\psi}\)}^\ast\fbox{\(\psi\)}) \\ \cC(\varphi\ \TFsince\ \psi) \!\!\!& \TFbd{=} &\!\!\! \cC(\varphi\ \TFsinc\ \psi) \cap (\fbox{\(\varphi\ \TFsince\ \psi\)}\Rightarrow\fbox{\(\psi\)} | \fbox{\(\varphi,\ \varphi\ \TFsinc\ \psi\)} ) \\ \cC(\varphi\ \TFsinc\ \psi) \!\!\!& \TFbd{=} &\!\!\! \cC(\varphi) \cap \cC(\psi) \cap (\fbox{\(\varphi\ \TFsinc\ \psi\)}\stackrel{{\sf b}}\Rightarrow \fbox{\(\psi\)}\fbox{\(\varphi\vphantom{\psi}\)}^\ast) \end{eqnarray*}

and for p ∈ P,

\begin{eqnarray*} \cC(p) \TFbd{=} \fbox{\TFnow}\fbox{\(\vphantom{\TFnow}\)}^{\ast}\fbox{\TFnow} \ \Ra \ \emptyset \end{eqnarray*}

saying the fluent now occurs at most once. Next, we intersect 𝓒(ϕ) with the set $\(\tuple{\unrhdSQ}\fbox{\)\TFnow,\varphi\(}\)$ of strings in which ϕ and now occur in a box, to form

\begin{eqnarray*} \cA_\circ(\varphi) \TFbd{=} {\cC}(\varphi)\cap \tuple{\unrhdSQ}\fbox{\(\TFnow,\varphi\)}. \end{eqnarray*}

But what alphabet Pow(Φ) are we assuming for 𝓒(ϕ) and $\(\tuple{\unrhdSQ}\fbox{\)\TFnow,\varphi\(}\)?$ Φ had better be finite if the Peirce product 〈⊑〉L is to be regular. It suffices (for our purposes) to let Φ be the finite subset Ψ(ϕ) of P + ∪ {now} consisting of ϕ and formulas mentioned in the definition of 𝓒(ϕ) — roughly ϕ, its subformulas and (now). For example,

\begin{eqnarray*} \Psi(\varphi\vee \psi) \!\!\!& = &\!\!\! \{\varphi\vee\psi\}\cup \Psi(\varphi)\cup\Psi(\psi) \\ \Psi(\varphi\ \TFsince\ \psi)\!\!\! & = & \!\!\! \{\varphi\ \TFsince\ \psi\}\cup \Psi(\varphi\ \TFsinc\ \psi) \\ \Psi(\varphi\ \TFsinc\ \psi) \!\!\!& = &\!\!\! \{\varphi\ \TFsinc\ \psi\}\cup \Psi(\varphi) \cup \Psi(\psi) \\ \Psi(p) \!\!\!& = &\!\!\! \{p,\TFnow\} \end{eqnarray*}

so that for p,q,r ∈ P,

\begin{eqnarray*} \Psi((p\vee q)\ \TFsince\ \TFnext(r)) \!\!\!& = &\!\!\! \{(p\vee q)\ \TFsince\ \TFnext(r),\ (p\vee q)\ \TFsinc\ \TFnext(r), \\ & & \ \ p\vee q, \ \TFnext(r), \ p, q, r, \TFnow\}. \end{eqnarray*}

Even with the alphabet restricted, the language 𝒜°(ϕ) is quite massive. But we can reduce it a couple of ways. The first is through ⊵-minimization: given a language L, define the set L ⊵ of ⊵-minimal strings in L by

\begin{eqnarray*} L_{\unrhd} \TFbd{=} L- \tuple{\rhd}L, \end{eqnarray*}

where ⊳ is ⊵ minus equality

\begin{eqnarray*} \sss \rhd \sss' \TFbd{\iff} \sss\unrhd \sss' \mbox{and} \sss\neq \sss'. \end{eqnarray*}

For example,

\begin{eqnarray*} (\square^\ast | L)_{\unrhd} = \square^\ast. \end{eqnarray*}

Notice that L ⊵ is regular if L is (as a finite-state transducer for ⊳ can be easily obtained from the one above for ⊵ by requiring that there be a proper inclusion ⊃). The second way of trimming a language is by projecting every string α1···αn in it to the string

\begin{eqnarray*} \rho(\alpha_1\cdots \alpha_n) \TFbd{=} (\alpha_1\cap (P\cup\{\TFnow\}))\cdots (\alpha_n\cap (P\cup\{\TFnow\})) \end{eqnarray*}

restricting the symbols to subsets of P ∪ {now}. For instance, if p ∈ P then

\begin{eqnarray*} \rho(\fbox{\(p,\psi\vee\varphi\)}\fbox{\(\TFnow,\TFprev(\chi)\)}) = \fbox{\(p\vphantom{\psi}\)}\fbox{\(\TFnow\vphantom{\psi p}\)}. \end{eqnarray*}

Clearly, as a relation, ρ is regular. Now, for ϕ ∈ P +, we take the ⊵-minimal strings in 𝒜°(ϕ), and apply ρ and unpad in succession to form

\begin{eqnarray*} \cA[\varphi] \TFbd{=} \{\unpad(\rho(\sss))\ |\ \sss\in \cA_\circ(\varphi)_{\unrhd}\}. \end{eqnarray*}

From the closure properties of regular languages, it follows that 𝓐[ϕ] is regular, as is $\(\cR[\varphi]=\tuple{\sqsubseteq}\cA[\varphi]\)$. To relate 𝓐[ϕ] to LTL, let us adopt the obvious interpretation of the connectives ntil

\begin{eqnarray*} V,t\models \varphi\ \TFntil\ \psi \!\!\!\!\!& \TFbd{\iff} & \!\!\!\!\! (\exists t'>t)\ V,t'\models \psi \mbox{and} \\ & & \hspace{.55in} \mbox{whenever} t< t''< t', \ V,t''\models \varphi \end{eqnarray*}

and sinc

\begin{eqnarray*} V,t\models \varphi\ \TFsinc\ \psi \!\!\!\!\! & \TFbd{\iff} & \!\!\!\!\! (\exists t'<t)\ V,t'\models \psi \mbox{and} \\ & & \hspace{.55in} \mbox{whenever} t'< t''< t, \ V,t''\models \varphi \ \end{eqnarray*}

against relations V⊆𝕫 × P and integers t ∈ 𝕫). Moreover, as 0 is not one of the fluents out of which we construct strings in 𝓐[ϕ], we delete the fluent 0 in our encoding str(s,t) of a finite relation s ⊆ 𝕫 × P and an integer t ∈ 𝕫 to form the string str°(s,t). For example,

\begin{eqnarray*} \TFstr_\circ(\{(-1,p),(-1,q),(2,r)\},1)\!\!\! & = &\!\!\! \fbox{\(p,q\)}\fbox{\(\vphantom{p,q}\)}\fbox{\TFnow\(\vphantom{p}\)} \fbox{\(r\vphantom{p}\)} \\ & = &\!\!\! \TFstr_\circ(\{(-2,p),(-2,q),(1,r)\},0) \end{eqnarray*}

illustrating the possibility that now can be set without loss of generality to 0.Footnote 5 To establish the faithfulness of the about sets 𝓐[ϕ] to LTL, we can prove by induction on ϕ ∈ P + that

Theorem. For all $\(\varphi\in P_+\), \(V\subseteq{\ZZ}\times P\) and \(t\in \ZZ\),\/}$

\begin{eqnarray*} V,t\models \varphi \iff (\exists s\subseteq V)\ \TFstr_\circ(s,t) \in \cA[\varphi]. \end{eqnarray*}

2.4 Irregular replace

All the clean-up on 𝒜°(ϕ) above just to extract 𝓐[ϕ] invites the question: why not define a regular relation unwinding a non-atomic formula ϕ rather than a regular language 𝓐[ϕ] via a system of constraints and projections? (Or for readers familiar with Beesley and Karttunen (Reference Beesley and Karttunen2003), why not replace, rather than constrain?) Take, for example, the formula Pp saying p holds now or sometime in the past. It is easy enough to construct a finite-state transducer for a relation $\hat{R}$ replacing Pp by p or shifting Pp backwards one square so that, for example,

\begin{eqnarray*} \fbox{\(\vphantom{Pq}\)}\fbox{\( {\sf P}p,q\)} \ \hat{R} \ \fbox{\(\vphantom{Pq}\)} \fbox{\(p,q\vphantom{P}\)} & \mbox{and} & \fbox{\(\vphantom{Pq}\)}\fbox{\( {\sf P}p,q\)} \ \hat{R} \ \fbox{\( {\sf P}p\)} \fbox{\(q\vphantom{P}\)}. \end{eqnarray*}

Repeatedly applying $\hat{R}$, let tc($\hat{R}$) be the transitive closure of $\hat{R}$. We have for all non-negative integers m and n,

\begin{eqnarray*} \fbox{\(\vphantom{Pp}\)}^{m+n+1} \fbox{\( {\sf P}p,q\)} & {\rm tc}(\hat{R}) & \fbox{\(\vphantom{Pp}\)}^m\fbox{\(p\vphantom{P}\)} \fbox{\(\vphantom{Pp}\)}^n\fbox{\(q\vphantom{Pp}\)}. \end{eqnarray*}

The difficulty, however, is tc($\hat{R}$) is not regular, even though $\hat{R}$ is. To see this, consider feeding strings from the language $\fbox{\)\vphantom{Pp}\(}^\ast\fbox{{\sf P}p,q\(}^\ast\)$ as inputs to tc($\hat{R}$). What output strings do we get that belong in the language $\(\fbox{\)p\(}^+\fbox{\)q\(}^+$ (where $L^+ \TFbd{=} L^\ast L$, as usual)? As each input string $\fbox{\)\vphantom{Pp}\(}^m\fbox{\) {\sf P} p, q\(}^n$ can move at most n p's into $\square^m$, there can be no more $\fbox{p}'$s than $\fbox{q}'$s in an output string, and we have

\begin{eqnarray*} \{\sss'\ | \ (\exists \sss\in \fbox{\(\vphantom{Pp}\)}^\ast\fbox{\( {\sf P}p,q\)}^\ast)\ \sss\ {\rm tc}(\hat{R})\ \sss'\} \ \cap\ \fbox{p}^+\fbox{q}^+ = \{\fbox{p}^m\fbox{q}^n \ | \ 1\leq m\leq n\} \end{eqnarray*}

which is non-regular. It follows that tc($\hat{R}$) cannot be a regular relation since the languages $\(\fbox{\)p\(}^+\fbox{\)q\(}^+$ and $\fbox{\)\vphantom{Pp}\(}^\ast\fbox{\) P p,q\(}^\ast$ are regular. By contrast, constraints applied with $\(\unrhd$-minimization and unpad intersect with $\(\fbox{\)p\(}^+ \fbox{\)q\(}^+$ to give the regular sublanguage $\fbox{\)p\(}\fbox{\)q\(}^+$.

3 Conclusion

Regular relations 𝓡[ϕ] were defined for various absolute LTL formulas ϕ (collected in the set P +) from regular languages 𝓐[ϕ] satisfying constraints 𝒞(ϕ) that essentially reformulate well-known LTL tableau rules in finite-state terms. A theorem was isolated at the end of Section 2.3 asserting that 𝓐[ϕ] encodes satisfaction ⊧ relative to arbitrary relations V ⊆ 𝕫 × P over the full set 𝕫 of integers. The theorem is not surprising, but introduces machinery that is, I believe, of interest beyond the theorem. That said, the theorem does raise further questions about the relationship with LTL. Can we apply the about sets 𝓐[ϕ] to capture LTL entailments ├LTL between formulas in P +? What about non-absolute LTL formulas such as Gp? We turn to these questions below, before briefly touching one of the points behind introducing regular relations 𝓡[ϕ]—i.e., that of varying temporal granularity.

3.1 Entailments short of ├LTL

A problem with reducing LTL entailments

\begin{eqnarray*} \varphi \boxvr^{{\rm LTL}} \psi \TFbd{\iff} (\forall V\subseteq \times P)\,(\forall t\in) \ V,t\models \varphi \implies V,t\models \psi\ \end{eqnarray*}

to 𝒜[ϕ] ⊑ 𝓐[ψ] is that a string in 𝓐[ϕ] may be too small to contain one in 𝒜[ψ]. Accordingly, the entailment

\begin{eqnarray*} \varphi \boxvr_C \psi \iff C\cap\tuple{\sqsubseteq}\cA[\varphi] \ \subseteq\ \tuple{\sqsubseteq}\cA[\psi] \end{eqnarray*}

enlarges a string in 𝓐[ϕ] to one in C before searching for a (sub)string in 𝒜[ψ]. Each string, however, has a bounded temporal span short of 𝕫, representable as a finite segment

\begin{eqnarray*} [i,j] \TFbd{=} \{t\in \ | \ i\leq t\leq j\} \end{eqnarray*}

for i, j ∈ 𝕫. In effect, V, t ⊧ ϕ is replaced by

\begin{eqnarray*} s,t \models_i^j \varphi \quad \mbox{for} \quad s\subseteq [i,j] \times P \mbox{and} t\in[i,j],\ \end{eqnarray*}

where for example,

\begin{eqnarray*} s,t \models_i^j \TFnext(\phiv!\!\!\!\! & \TFbd{\iff} &\!\!\!\!\! t<j \mbox{and} s,t+1 \models_i^j\varphi\ \\ s,t \models_i^j \TFprev(&#x03D5;!\!\!\!\! & \TFbd{\iff} &\!\!\!\!\! i<t \mbox{and} s,t-1 \models_i^j\varphi \end{eqnarray*}

and

\begin{eqnarray*} s,t \models_i^j {\sf G}\varphi \TFbd{\iff} (\forall t'\in [t,j])\ s,t' \models_i^j\varphi. \end{eqnarray*}

For non-negative integers m and n, let Cmn be the constraint

\begin{eqnarray*} C_m^n \TFbd{=} (\fbox{\TFnow} \stackrel{{\sf b}}{\Rightarrow} \fbox{\(\vphantom{\TFnow}\)}^m) \ \cap \ (\fbox{\TFnow} \stackrel{{\sf a}}{\Rightarrow} \fbox{\(\vphantom{\TFnow}\)}^n) \ \cap \ (\fbox{\TFnow} \fbox{\(\vphantom{\TFnow}\)}^\ast\fbox{\TFnow} \Ra \emptyset) \end{eqnarray*}

requiring that there be at least m boxes before the evaluation time now and n boxes after, and at most one occurrence of now. Then for ϕ, ψ ∈ P +,

(21)
\begin{eqnarray} \label{cnm} \varphi \boxvr_{C_m^n}\psi \!\!\!\!\!& \iff & \!\!\!\!\! (\forall i\leq -m) (\forall j\geq n) (\forall s\subseteq [i,j] \times P) \\ \nonumber & & \hspace{.4in} s,0\models^j_i\varphi \ \implies\ s,0\models^j_i\psi \end{eqnarray}

with now normalized to 0 to simplify notation. To build the negation p of an atomic proposition p into P, we intersect Cmn with the constraint

\begin{eqnarray*} (\fbox{\(\vphantom{\overline{p}}\)} \Rightarrow \fbox{\(p\vphantom{\overline{p}}\)} \ | \ \fbox{\(\overline{p}\)}) \cap (\fbox{\(p,\overline{p}\)} \Rightarrow \emptyset) \end{eqnarray*}

corresponding to a restriction in (21) to relations s ⊆ [i,j] × P satisfying

\begin{eqnarray*} s(t,\overline{p}) \iff \mbox{not} s(t,p) \end{eqnarray*}

for t ∈ [i,j]. Observe that next n(p ∨ p) holds at 0 for any such relation s,

\begin{eqnarray*} s,0 \models^j_i \TFnext^{n}(p\vee\overline{p}) \end{eqnarray*}

but not necessarily next n+1(p ∨ p). Similarly for previous m(p ∨ p).

Stepping beyond absolute formulas, notice that the LTL entailment

\begin{eqnarray*} {\sf G}p \boxvr^{{\rm LTL}} {\sf G}\ \TFnext(p) \end{eqnarray*}

(saying ‘if p is true now and forever more, then so is next(p)’) does not go through for ├C (unless C precludes Gp), as

\begin{eqnarray*} s,t \not\models_i^j {\sf G}\ \TFnext(p) \end{eqnarray*}

for all s ⊆ [i,j] × P and t ∈ [i,j].

3.2 Gp and some other non-absolute formulas

To say Gp is not absolute is to deny that 𝓡[Gp] can be the 𝒜[Gp]-restriction of ⊒, whatever 𝒜[Gp] might be. But if, in place of ⊑, we define a relation $\hat{R}$ by

\begin{eqnarray*} \sss\ \hat{R}\ \sss' \TFbd{\iff} (\exists \sss'')\ \sss\unrhd \sss''\sss' \end{eqnarray*}

(sandwiched between ⊒ and $\unrhd$) and put

\begin{eqnarray*} \cA[{\sf G}p] \TFbd{=} \fbox{\(\TFnow,p\)}\fbox{{\it p}}^\ast\ \end{eqnarray*}

then we can set 𝓡[Gp] to the 𝒜[Gp]-restriction of $\hat{R}$

\begin{eqnarray*} \sss\ \cR[{\sf G}p]\ \sss' \TFbd{\iff} \sss\ \hat{R}\ \sss' \mbox{and} \sss'\in {\cA[{\sf G}p]}. \end{eqnarray*}

Similarly, for the past counterpart H of G with the semantic interpretation

\begin{eqnarray*} s,t \models_i^j {\sf H}\varphi \TFbd{\iff} (\forall t'\in [i,t])\ s,t' \models_i^j\varphi \end{eqnarray*}

let

\begin{eqnarray*} \cA[{\sf H}p] \TFbd{=} \fbox{\it p}^\ast\ \fbox{\(\TFnow,p\)} \end{eqnarray*}

and

\begin{eqnarray*} \sss\ \check{R}\ \sss' \TFbd{\iff} (\exists \sss'')\ \sss\unrhd \sss'\sss'' \end{eqnarray*}

for

\begin{eqnarray*} \sss\ \cR[{\sf H}p]\ \sss' \TFbd{\iff} \sss\ \check{R}\ \sss' \mbox{and} \sss'\in {\cA[{\sf H}p]}. \end{eqnarray*}

Generalizing over Gp and Hp, we can use $\unrhd$ in place of ⊑, $\hat{R}$ or Ř, provided we pad 𝒜[Gp] to the left for

\begin{eqnarray*} \cA'[{\sf G}p] \TFbd{=} \fbox{\(\vphantom{p}\)}^\ast\ \fbox{\(\TFnow,p\)}\fbox{\it p}^\ast\ \end{eqnarray*}

and 𝒜[Hp to the right for

\begin{eqnarray*} \cA'[{\sf H}p] \TFbd{=} \fbox{\it p}^\ast\ \fbox{\(\TFnow,p\)} \fbox{\(\vphantom{p}\)}^\ast \end{eqnarray*}

so that

(22)
\begin{eqnarray*} \label{unrhd} \sss\ &#x1D4E1;[&#x03D5;] \sss' \TFbd{\iff} \sss\unrhd \sss' \mbox{and} \sss'\in\cA'[\varphi]. \end{eqnarray}

Under (22), 𝒜′[ϕ] need not be padded

\begin{eqnarray*} \cA'[{\sf H}p\wedge {\sf G}q] \TFbd{=} \fbox{\it p}^\ast \fbox{\(\TFnow,p,q\)} \fbox{\it q}^\ast \end{eqnarray*}

although for absolute formulas, the price of strengthening ⊒ to $\unrhd$ is padding to the left and rightFootnote 6

\begin{eqnarray*} \cA'[\varphi] \TFbd{=} \square^\ast \cA[\varphi] \square^\ast \quad \mbox{for} \varphi\in P_+ \end{eqnarray*}

(undoing the step from ⊒ to $\unrhd$). Padding goes against the grain of defining 𝓡[ϕ] to get a handle on the temporal span of a ϕ-situation (useful, for example, for past tense reports; recall Section 1.4 above). On the other hand, it is easy enough to unpad 𝒜′[ϕ] for 𝓐[ϕ].

3.3 From temporal span to grain

If the image of 𝓡[ϕ] is unpadded, then we can replace ⊒ by ⊒° inasmuch as

\begin{eqnarray*} \sss\ \sqsupseteq\ \sss' \iff \sss\ \sqsupseteq_\circ\ \sss' \quad \mbox{if} \unpad(\sss') =\sss', \end{eqnarray*}

where

\begin{eqnarray*} \sss\ \sqsupseteq_\circ\ \sss' \TFbd{\iff} \sss\ \mbox{{\sf has-factor}} ; \unrhd\ \sss' \ \end{eqnarray*}

and factors are suffixes of prefixes (equivalently, prefixes of suffixes)

\begin{eqnarray*} \sss\ \mbox{{\sf has-factor}}\ \sss' \!\!\!\!\! \iff &\!\!\!\!\! \sss\ \mbox{{\sf has-prefix}} \mbox{{\sf has-suffix}} \ \sss' \\ \iff &\!\!\!\!\! \sss\ \mbox{{\sf has-suffix}} \mbox{{\sf has-prefix}} \ \sss' \ \end{eqnarray*}

and a suffix is a tail end

\begin{eqnarray*} \sss\ \mbox{{\sf has-suffix}}\ \sss' \TFbd{\iff} (\exists \sss'')\ \sss = \sss''\sss' \end{eqnarray*}</p>

and a prefix is an initial fragment

\begin{eqnarray*} \sss\ \mbox{{\sf has-prefix}}\ \sss' \TFbd{\iff} (\exists \sss'')\ \sss = \sss'\sss''. \end{eqnarray*}

The ‘in’ relation $\hat{R}$ for Gp replaces has-factor by has-suffix

\begin{eqnarray*} \sss\ \hat{R}\ \sss' \TFbd{\iff} \sss\ \mbox{{\sf has-suffix}} ; \unrhd\ \sss' \end{eqnarray*}

while the ‘in’ relation Ř for Hp uses has-prefix

\begin{eqnarray*} \sss\ \check{R}\ \sss' \TFbd{\iff} \sss\ \mbox{{\sf has-prefix}} ; \unrhd\ \sss'. \end{eqnarray*}

That said, an advantage of the formulation ⊒ over ⊒°

\begin{eqnarray*} \sss\ \sqsupseteq \sss' \TFbd{\iff} (\exists \sss_\circ \approx \sss) (\exists \sss'_\circ \approx \sss') \ \sss_\circ \unrhd \sss'_\circ \end{eqnarray*}

(where $\sss_circ\approx\sss \TFbd{\iff} \unpad(\sss_circ) = \unpad({\sc s}))\)$ is that it generalizes from unpad to an arbitrary function π (Table 4).

Table 4.

Comparing information content modulo π.

An example of π suggested by the slogan ‘no time without change’ (Kamp and Reyle Reference Kamp and Reyle1993: 674) reduces all adjacent identical boxes ααn to one α. More precisely, the block compression bc(s) of a string s is given by

\begin{eqnarray*} \TFbc(\sss) \TFbd{=} \left\{ \begin{array}{@{}l@{\quad}l@{}} \TFbc(\alpha\sss') & \mbox{if} \sss=\alpha\alpha\sss' \\ \alpha\TFbc(\beta\sss') & \mbox{if} \sss=\alpha\beta\sss' \mbox{with} \alpha\neq\beta \\ \sss & \mbox{otherwise (length$(\sss)\leq 1$)} \end{array}\right. \end{eqnarray*}

so that, for example,

\begin{eqnarray*} \TFbc(\fbox{\(p,q\)}\fbox{\(p,q\)}\fbox{\(p,q\)} \fbox{\(p,q,r\)}\fbox{\(p,q,r\)}\fbox{\(p,q\)}) = \fbox{\(p,q\)}\fbox{\(p,q,r\)}\fbox{\(p,q\)}. \end{eqnarray*}

For a finite-state transducer computing bc, let the set of states be the alphabet plus the initial state 0, with transitions

\begin{eqnarray*} &0 \stackrel{\alpha:\alpha}{\to} \alpha \quad \mbox{for every symbol} \alpha \\ &&\alpha \stackrel{\beta:\beta}{\to} \beta \quad \mbox{for any two distinct symbols} \alpha, \beta \end{eqnarray*}

(to remember the symbol last seen)

\begin{eqnarray*} \alpha \stackrel{\alpha:\epsilon}{\to} \alpha \quad \mbox{for every symbol} \alpha \end{eqnarray*}

(to remove duplications) and all states final (accepting). If a string s is construed as a sequence of observations, the effect of bc(s) is to keep time still if no change (from the previous box) is observed. Exactly what observations are allowed is the crucial issue of granularity, which amounts in the present context to what fluents may occur in a symbol α. The LTL connective previous makes each tick of the clock 𝕫 count as an observation, thereby neutralizing bc. For instance, the string $\fbox{\it p}\fbox{\it p}\fbox{\it p}}$ is treated in LTL as

\begin{eqnarray*} \fbox{\(p\vphantom{(p)}\)}\fbox{\(p,\TFprev(p)\)}\fbox{\(p, \TFprev(\TFprev(p))\)} \end{eqnarray*}

which bc leaves unchanged, whereas $\TFbc(\fbox{\)p\(}\fbox{\)p\(}\fbox{\)p\(}) = \fbox{\)p\(}$. Evidently, we must apply block compression on a string only if it records all information of interest explicitly as fluents. As our interests may change, it is useful to define for any set X ⊑ Φ) of fluents, a function ρX on strings that restricts the observations to X by intersecting componentwise with X

\begin{eqnarray*} \rho_X(\alpha_1\alpha_2\cdots\alpha_n)\!\!\! & \TFbd{=} &\!\!\! (\alpha_1\cap X)(\alpha_2\cap X)\cdots(\alpha_n\cap X). \end{eqnarray*}

For example, if X = {Jan, Feb,. . ., Dec}, ρX projects the string

\begin{eqnarray*} \fbox{{\sf Jan,d1}}\fbox{{\sf Jan,d2}} \cdots \fbox{{\sf Feb,d29}}\fbox{{\sf Mar,d1}}\cdots \fbox{{\sf Dec,d31}} \end{eqnarray*}

(over the 43 fluents Jan, Feb,. . ., Dec, d1, d2,. . ., d31) representing a leap year to

\begin{eqnarray*} \fbox{{\sf Jan}}^{31} \fbox{{\sf Feb}}^{29}\fbox{{\sf Mar}}^{31}\cdots \fbox{{\sf Dec}}^ {31}\ \end{eqnarray*}

which bc maps to the string

\begin{eqnarray*} \fbox{{\sf Jan}} \fbox{{\sf Feb}}\fbox{{\sf Mar}}\cdots \fbox{{\sf Dec}} \end{eqnarray*}

of length 12. Composing ρX; bc further with unpad gives regular relations

\begin{eqnarray*} \pi_X(\sss) \TFbd{=} \unpad(\TFbc(\rho_X(\sss))) \end{eqnarray*}

relative to which event structures (in the sense of Kamp and Reyle Reference Kamp and Reyle1993) can be constructed as inverse (projective) limits over finite sets X of fluents (Fernando Reference Fernando2007, Reference Fernando2010). Integrating calendar expressions with temporal propositions, the basic idea is to work with strings that have no more and no less information than what is given. Natural language descriptions do not, as a rule, mention a clock, and rarely the clock 𝕫 (however natural that may be for LTL applications).

Acknowledgments

I thank my referees for their critical and constructive comments, and Anssi Yli-Jyrä for his work as editor.

Footnotes

1 That is, negation is pushed down to the level of atomic formulas using De Morgan's laws and counter-extensions.

2 The shortcomings of this semantics as an account of English until are irrelevant to the present point; the reader is free to rename the connective characterized by the clause.

3 A Reichenbachian account of tense and aspect that is free from this Priorean defect is formulated in terms of strings in section 2 of Fernando (Reference Fernando2008a).

4 The terminology ‘Peirce product’ is from Brink, Britz, and Schmidt (Reference Brink, Britz and Schmidt1994), but the notation 〈R〉L is borrowed from dynamic logic (Harel et al. Reference Harel, Kozen and Tiuryn2000).

5 That is, for all LTL-formulas ϕ, relations V ⊆𝕫 × P and integers t,

\begin{eqnarray*} V,t\models \varphi \iff V_t,0\models\varphi \end{eqnarray*}

where Vt is V shifted to the right by t

\begin{eqnarray*} V_t \TFbd{=} \{(t'-t,p) \ | \ V(t',p)\}. \end{eqnarray*}

From the perspective of Hybrid Logic (Areces and ten Cate Reference Areces, ten, Blackburn, Wolter and van Benthem2007), LTL lacks a nominal marking out the position 0.

6 This is exactly analogous to the transformation of a stringwise representation L to the pathwise representation $\square^\ast L\square^\ast$ in Fernando (Reference Fernando, Hanneforth and Würzner2008b).

References

Areces, C. and tenCate, B. Cate, B. 2007. Hybrid logics. In Blackburn, P., Wolter, F., and van Benthem, J. (eds.), Handbook of Modal Logic, pp. 821–68. Amsterdam, The Netherlands: Elsevier.CrossRefGoogle Scholar
Barwise, J. and Perry, J. 1983. Situations and Attitudes. Cambridge, MA, USA: The MIT Press.Google Scholar
Beesley, K. R. and Karttunen, L. 2003. Finite State Morphology. Stanford, CA, USA: CSLI Publications.Google Scholar
Bouajjani, A., Jonsson, B., Nilsson, M. and Touili, T. 2000. Regular model checking. In Computer Aided Verification, pp. 403–18. LNCS 1855. Berlin, Germany: Springer-Verlag.CrossRefGoogle Scholar
Brink, C., Britz, K. and Schmidt, R. 1994. Peirce algebras. Formal Aspects of Computing 6 (3):339–58.CrossRefGoogle Scholar
Condoravdi, C. 2009. Punctual until as a scalar NPI. In Hanson, K., and Inkelas, S. (eds.), The Nature of the Word: Studies in Honor of Paul Kiparsky, pp. 631–53. Cambridge, MA, USA: The MIT Press.Google Scholar
Davidson, D. 1967. The logical form of action sentences. In Rescher, N. (ed.), The Logic of Decision and Action, pp. 81–95. Pittsburgh, PA, USA: University of Pittsburgh Press.Google Scholar
Emerson, E. A. 1992. Temporal and modal logic. In van Leeuwen, J. (ed.), Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, pp. 995–1072. Cambridge, MA, USA: The MIT Press.Google Scholar
Fernando, T. 2004. A finite-state approach to events in natural language semantics. Journal of Logic and Computation 14 (1): 79–92.CrossRefGoogle Scholar
Fernando, T. 2007. Observing events and situations in time. Linguistics and Philosophy 30 (5): 527–50.CrossRefGoogle Scholar
Fernando, T. 2008a. Branching from inertia worlds. Journal of Semantics 25 (3): 321–344.CrossRefGoogle Scholar
Fernando, T. 2008b. Temporal propositions as regular languages. In Hanneforth, T., and Würzner, K-M. (eds.), Finite-State Methods and Natural Language Processing, 6th International Workshop, pp. 132–48. Potsdam, Germany: Universitätsverlag Potsdam.Google Scholar
Fernando, T. 2009a. Situations in LTL as strings. Information and Computation 207 (10): 980–99.CrossRefGoogle Scholar
Fernando, T. 2009b. Situations as indices and as denotations. Linguistics and Philosophy 32 (2): 185–206.CrossRefGoogle Scholar
Fernando, T. 2010. Constructing situations and time. Journal of Philosophical Logic, doi:10.1007/s10992-010-9155-1.Google Scholar
Harel, D., Kozen, D. and Tiuryn, J. 2000. Dynamic Logic. Cambridge, MA, USA: The MIT Press.CrossRefGoogle Scholar
Kamp, H. and Reyle, U. 1993. From Discourse to Logic. Dordrecht: Kluwer.Google Scholar
Karttunen, L. 1974 Until. In Papers from the Tenth Regional Meeting of the Chicago Linguistic Society, Chicago, pp. 284–97.Google Scholar
Karttunen, L. 2005 The Yale Shooting Problem. http://www.stanford.edu/~laurik/fsmbook/examples/YaleShooting.htmlGoogle Scholar
McCarthy, J. and Hayes, P. 1969. Some philosophical problems from the standpoint of artificial intelligence. In Meltzer, M., and Michie, D. (eds.), Machine Intelligence 4, pp. 463–502. Edinburgh, UK: Edinburgh University Press.Google Scholar
Mulligan, K., Simons, P. and Smith, B. 1984. Truth-makers. Philosophy and Phenomenological Research 44: 287–321.CrossRefGoogle Scholar
Niemi, J. and Koskenniemi, K. 2009. Representing and combining calendar information by using finite-state transducers. In Piskorski, J., Watson, B., and Yli-Jyrä, A. (eds.), Finite-State Methods and Natural Language Processing: Post-proceedings of the 7th International Workshop FSMNLP 2008, pp. 122–33. Amsterdam, The Netherlands: IOS Press.Google Scholar
Reichenbach, H. 1947. Elements of Symbolic Logic. London, UK: Macmillan.Google Scholar
Vardi, M. Y. 2007. Automata-theoretic techniques for temporal reasoning. In Blackburn, P., Wolter, F., and van Benthem, J. (eds.), Handbook of Modal Logic, pp. 971–89. Amsterdam, The Netherlands: Elsevier.CrossRefGoogle Scholar
Figure 0

Table 1. Basic notions from an intension function 𝓘[ϕ].

Figure 1

Table 2. Some regular notions given a regular language L and relation R.

Figure 2

Table 3. Comparing information content

Figure 3

Table 4. Comparing information content modulo π.