The Transformation Logics

1 Introduction

We introduce the Transformation Logics, a new family of temporal logics designed to finely balance the trade-off between expressivity and complexity. Their key feature is the possibility of defining operators of a new kind that we call transformation operators. They capture patterns over sequences, and they can be thought of as a generalisation of temporal operators. The subclass of transformation operators based on finite semigroups is of particular interest. Such semigroup-like operators suffice to capture all regular languages, and remarkably they allow for creating hierarchies of increasing expressivity and complexity which are non-trivial to define in existing logics. The base level of such hierarchies is obtained using the operator defined by the flip-flop monoid. The other levels are obtained introducing operators based on simple groups-the building blocks of all groups. Simple groups have been systematically classified into a finite number of families, cf. [Gorenstein , 2018 ]. The classification provides a compass in the landscape of groups, and a roadmap in the exploration of temporal logics, as it is made clear by the results in this paper.

Our motivation arises from the usage of temporal logics in AI. They are used in reinforcement learning to specify reward and dynamics functions [Bacchus et al., 1996; Brafman et al.,

2018; Icarte et al., 2018; Camacho et al., 2019; De Giacomo et al., 2020b; De Giacomo et al., 2020a]; in planning for describing temporally-extended goals [Torres and Baier, 2015; Camacho et al., 2017; De Giacomo and Rubin, 2018; Brafman and De Giacomo, 2019; Bonassi et al., 2023]; in stream reasoning to express programs with the ability of referring to different points of a stream of data [Beck et al., 2018; Ronca et al., 2022; Walega et al., 2023].

In the above applications, the required trade-off between expressivity and complexity will depend on the case at hand. When the basic expressivity of the star-free regular languages suffices, one can employ logics such as Past LTL [Manna and Pnueli, 1991] and LTLf [De Giacomo and Vardi, 2013]. In all the other cases, one needs to resort to more expressive logics. The existing extensions of the above logics have the expressivity of all regular languages, cf. ETL [Wolper, 1983] and LDLf [De Giacomo and Vardi, 2013]. This is a big leap in expressivity, which may incur an unnecessarily high computational complexity. We show next two examples where the required expressivity lies in fragments between the star-free regular languages and all regular languages. These fragments can be precisely characterised in the Transformation Logics.

Example 1. An agent is assigned a task that can be completed multiple times. We receive an update every minute telling us whether the agent has completed the task in the minute that has just elapsed. We need to detect whether the agent has completed the task at least once on every past day.

The example describes a periodic pattern, which is beyond the star-free regular languages. It requires to count minutes modulo 24 ∗ 60 = 1440 in order to establish the end of every day. This can be expressed in the Transformation Logics using a transformation operator defined by the cyclic group C1440. Cyclic group operators yield an ability to capture many useful periodic patterns. At the same time, they belong to the special class of solvable group operators, which enjoys good properties such as a more favourable computational complexity compared to larger classes of operators. The next one is an example where solvable group operators do not suffice, and we need to resort to symmetric group operators.

Example 2. A cycling race with n participants takes place, and we need to keep track of the live ranking. At each step an overtake can happen, in which case it is communicated to us in the form (i, i + 1) meaning that the cyclist in position i has overtaken the one in position i + 1. We know the initial ranking, and we need to keep track of the live ranking.

The ranking in the example corresponds to the symmetric group Sn, which is not solvable if n ≥ 5. The example can be specified in a Transformation Logic featuring a transformation operator defined by the group Sn.

Summary of the contribution. We introduce the Transformation Logics, providing a formal syntax and semantics. Their main characteristic is the transformation operators. The operators are very general, as we demonstrate through a series of concrete examples. We develop a systematic approach in defining operators, based on semigroup theory and algebraic automata theory, cf. [Ginzburg, 1968; Arbib, 1969; D¨om¨osi and Nehaniv, 2005]. This way we are able to identify prime operators that can capture all finite operators. For them, we prove a series of expressivity and complexity results. Regarding the expressivity, we show there exists one operator, defined by the flip-flop monoid, which yields the expressivity of the star-free regular languages; as one keeps adding operators based on cyclic groups of prime order, the expressivity increases, up to capturing all languages that can be captured using solvable group operators; the expressivity of all regular languages is reached by adding the other prime operators, that can be defined by choosing groups from the classification of finite simple groups, cf. [Gorenstein et al., 2018]. Regarding the complexity, we focus on the evaluation problem, and we show three sets of results. First, we show any Transformation Logic can be evaluated in polynomial time, whenever its operators can be evaluated in polynomial time. Second, for two notable families of operators, we show that polynomial-time evaluation is possible even when they are represented compactly. Third, we focus on the data complexity of evaluation showing that it corresponds to the three circuit complexity classes AC0 ⊊ ACC0 ⊆ NC1 when we include (i) only the flip-flop operator, (ii) also cyclic operators, and (iii) all operators. Finally, we show how Past LTL formulas can be easily translated into the core Transformation Logic featuring the flip-flop operator.

Extended version. Proofs of all our results as well as additional details on several aspects of the paper can be found in the extended version [Ronca, 2024].

2 Preliminaries

For X a set, a transformation is a function f : X → X. We write the identity function over any domain as id. We denote the Boolean domain {0, 1} by B, the natural numbers by N, and the integer numbers by Z.

2.1 Formal Languages

An alphabet Σ is a non-empty finite set of elements called letters. A string over Σ is a finite concatenation σ1 · · · σn of letters from Σ. A language over Σ is a set of strings over Σ. The regular languages are the ones languages that are defined by regular expressions, or equivalently by finite automata [Kleene, 1956]. The star-free regular languages are the languages that are defined by regular expressions without the Kleene star but with complementation, or equivalently by a group-free finite automaton, cf. [Ginzburg, 1968].

2.2 Propositional Logic

Syntax. A propositional variable is an element from a set V that we consider as given. Typically we denote propositional variables by lowercase Latin letters. A propositional formula is built out of propositional variables and the Boolean operators {¬, ∧, ∨}. It is defined inductively as a propositional variable or one of the following expressions: ¬α, α ∧ β, α ∨ β where α and β are propositional formulas. Additional Boolean operators may be defined, but it is not necessary as the former operators are universal, they suffice to express all Boolean functions.

Semantics. An interpretation I for a propositional formula is a subset of the propositional variables occurring in the formula. Intuitively, the fact that a variable appears in the intepretation means that the variable stands for a proposition that is true. An assignment is a function ν : V → B from a set of propositional variables V to the Boolean domain B = {0, 1}. When V = {v1, . . . , vn}, we can also write an assingment ν as the map ⟨v1, . . . , vn⟩ ↦→ ⟨b1, . . . , bn⟩, with the meaning that ν(vi) = bi. An interpretation I corresponds to the assignment ν such that ν(a) = 1 iff a ∈ I. Then, the semantics of formulas is defined in terms of the following satisfiability relation. Given a formula α and an interpretation I for α, the satisfiability relation I |= α is defined following the structural definition of formulas, for variables as

• I |= a iff a ∈ I,

and inductively for the other formulas as

• I |= ¬α iff I ̸|= α,
• I |= α∨ β iff I |= α or I |= β,
• I |= α∧ β iff I |= α and I |= β.

An assignment ν to variables {a1, . . . , am} can be seen as the conjunction l1 ∧ · · · ∧ lm where li = ai if ν(ai) = 1 and li = ¬ai otherwise. This allows us to write I |= ν.

2.3 Semigroups and Groups

A semigroup is a non-empty set together with an associative binary operation that combines any two elements a and b of the set to form a third element c of the set, written c = (a · b). A monoid is a semigroup that has an identity element e, i.e., (a · e) = (e · a) = a for every element a. The identity element is unique when it exists. A group is a monoid where every element a has an inverse b, i.e., (a·b) = (b·a) = e where e is the identity element. For every element a of a group, its inverse is unique and it is denoted by a-1 . A subsemigroup (subgroup) of a semigroup S is a subset of S that is a semigroup (group). The order of a semigroup is the number of elements. For S and T semigroups, we write ST = {s · t | s ∈ S, t ∈ T}; we also write S1 = S and Sn = SSn-1 . A semigroup S is generated by a semigroup T if S = ⋃n T n . A homomorphism from a semigroup S to a semigroup T is a mapping ψ : S → T such that ψ(s1 · s2) = ψ(s1) · ψ(s2) for every s1, s2 ∈ S. If ψ is bijective, we say that S and T are isomorphic. Isomorphic semigroups are considered identical. Let G be a group and let H be a subgroup of G. A right coset of G is g · H = {g · h | h ∈ H} for g ∈ G, and a left coset of G is H · g = {h · g | h ∈ H} for g ∈ G. Subgroup H is normal if its left and right cosets coincide. A group is trivial if it is the singleton {e}. A simple group is a group G such that every normal subgroup of G is either trivial or G itself. For g, h ∈ G, the commutator of g and h is g-1 · h-1 · g · h. The derived subgroup of G is the subgroup generated by its commutators. Setting G(0) = G, the n-th derived subgroup G(n) is the derived subgroup of G(n-1) . A group is solvable if there exists n such that G(n) is trivial.

A flip-flop monoid is a three-element monoid {s, r, e} where (r · s) = s, (s · s) = s, (r · r) = r, and (s · r) = r. All flip-flop monoids are isomorphic, and hence one refers to the flip-flop monoid. A cyclic group is a group that is isomorphic to the group Cn of integers {0, . . . , n-1} with modular addition i · j = i+j mod n. Again, one refers to any cyclic group of order n as the cyclic group Cn. Two relevant properties of cyclic groups are: (i) a cyclic group Cn is simple iff n is a prime number; (ii) every cyclic group is solvable.

3 The Transformation Logics

We introduce the Transformation Logics. They are a propositional formalism, atoms are variables standing for propositions that can be true or false. The truth of some variables is given as input, whereas the meaning of other variables is given by a definition. Definitions allow us to avoid nested expressions, and hence they aid intelligibility in this context. A definition features either a Boolean expression, the delay operator, or a transformation operator. The delay operator is akin to the before operator from Past LTL. A transformation operator has a domain of elements and a set of transformations over the domain-a transformation is a map from elements of a domain to elements of the same domain. At every step a transformation operator has an associated domain element to which it applies a transformation based on the truth value of the operands. Then the evaluation value is a function of the current domain element. Each transformation corresponds to a specific functionality. For example, setting a bit to one, or increasing a count. More intuition is given below in the Paragraph 'Explanation' and later in Section 3.1.

Syntax. A static definition is

where p is a propositional variable, and α is a propositional formula. A delay definition is

where p and q are propositional variables, and D is called the delay operator. A transformation operator T is a tuple ⟨X, T, ϕ, ψ⟩ consisting of a non-empty set X, a nonempty set T of transformations τ : X → X, a function ϕ : Bm → T, and a function ψ : X → Bn . We call X the transformation domain; we call m and n the input and output arity, respectively. An operator is finite if its transformation domain is finite-in which case all its other components are necessarily finite. A transformation definition is

where T is a transformation operator with input arity m and output arity n; p1, . . . , pn and q1, . . . , qm are variables; and x0 ∈ X is the initial domain element. A definition is either a static definition, a delay definition, or a transformation definition. In a definition, the expression on the left of ' :=' is called head, and the expression on the right is called body. A program is a finite set of definitions. A query is a pair (P, q) consisting of a program P and a variable q occurring in P. Programs are required to be nonrecursive, i.e., to have an acyclic dependency graph. The dependency graph of a program has one node for each variable in the program, and it has a directed edge from a to b if there is a definition where a is in the body and b is the head. Programs are also required to define variables at most once, i.e., every variable p occurs at most once in the head of a definition; if p occurs in the head of a definition d, we say that d defines p. In a given program P, a variable is a defined variable if there is a definition in P that defines it, and it is an input variable otherwise.

For T a set of transformation operators, the Transformation Logic L(T) is the set of programs consisting of all static definitions, all delay definitions, and all transformation definitions with operators from T.

Semantics. An input to a program P is a finite non-empty sequence of subsets of the input variables of P. An assignment to a transformation definition d is an expression d ↦→ x with x a domain element of the operator of d. The semantics of programs is defined in terms of the following satisfiability relation. Given a program P, an input I = I1, . . . , Iℓ to P, and an index t ∈ [1, ℓ], we define the satisfiability relation (P, I, t) |= E where E is a propositional variable, a propositional formula, or an assignment to a transformation definition. We assume definitions are in the form given above; it allows us to refer to the symbols mentioned there, e.g., symbol pi for the i-th head variable of a transformation definition.

1. For a an input variable,
2. (P, I, t) |= a iff a ∈ It;
3. For α and β formulas,
4. (P, I, t) |= ¬α iff (P, I, t) ̸|= α;
5. (P, I, t) |= α∨ β iff (P, I, t) |= α or (P, I, t) |= β;
6. (P, I, t) |= α ∧ β iff (P, I, t) |= α and (P, I, t) |= β;
7. For p a variable defined by a static definition,
8. (P, I, t) |= p iff (P, I, t) |= α;
9. For p a variable defined by a delay definition,
10. (P, I, t) |= p iff (P, I, t -1) |= q;
11. For d ↦→ x an assignment to a transformation definition d,
12. (P, I, 0) |= (d ↦→ x) iff x = x0; · (P, I, t) |= (d ↦→ x) iff - (P, I, t -1) |= (d ↦→ x′ ), - (P, I, t) |= (⟨q1, . . . , qm⟩ ↦→ µ), and - τ(x′ ) = x with τ = ϕ(µ);
13. For pi a variable defined by a transformation definition d,

• (P, I, t) |= (d ↦→ x), and
• ψ(x) = ⟨b1, . . . , bi, . . . , bn⟩ with bi = 1.

Explanation. The index t can be thought of as a time point, ranging over the positions of the given input I. Points 1 and 2 follow the standard semantics of propositional formulas, evaluated with respect to the assignment It. Points 3-5 define the semantics of definitions, relying on the auxiliary Point 6. Point 3 is the semantics of static definitions. It says that the truth value of a variable p defined by a static definitions is the truth value of the propositional formula α corresponding to the body of the definition, evaluated at the same time point. Point 4 is the semantics of delay definitions. It says that the truth value of a variable p defined by a delay definition is the truth value of the propositional variable q occurring in the body the definition, evaluated at the previous time point. Point 5 describes the element x that is currently associated with a transformation definition. For t = 0, the element is x0, the initial element specified in the definition. For t > 0, the element x is determined as follows. We pick an assignment ⟨q1, . . . , qm⟩ ↦→ µ for the body variables of the definition. Specifically, (P, I, t) |= (⟨q1, . . . , qm⟩ ↦→ µ) with µ = ⟨b1, . . . , bm⟩ means that (P, I, t) |= qi if bi = 1 and (P, I, t) ̸|= qi otherwise. The assignment determines the transformation τ = ϕ(µ), which in turn determines the next element x = τ(x′ ) from the previous one x′ . Point 6 defines the semantics of transformation definitions. It specifies when variables p1, . . . , pn defined by a transformation definition d are true. The semantics is defined considering a single variable pi at a time, considered as part of the former list. There is an element x of the transformation domain of T = ⟨X, T, ϕ, ψ⟩ that is currently associated with the definition d. Namely, the condition (P, I, t) |= (d ↦→ x) holds. Hence, the assignment ⟨b1, . . . , bn⟩ to the variables p1, . . . , pn is given by ψ(x).

3.1 Examples of Operators

The mechanism to define transformation operators allows for a great variety of operators. In this section we present several examples of transformation operators, showing that one can easily capture existing operators from the literature or design novel operators to capture known patterns on sequences.

Temporal Operators. We can define operators in the style of the temporal operators from Past LTL, cf. [Manna and Pnueli, 1991]. For instance, we can define the operator

where T consists of the transformations set(x) = 1 and id, and the function ϕ is defined as ϕ(0) = id and ϕ(1) = set. Then we can write a definition

which defines p as true when a has happened. Here the only meaningful choice of the initial transformation element is 0, and hence it can be omitted. Thus we can write the same definition as

with the understanding that it corresponds to the one above. Other temporal operators can be introduced in a similar way.

Threshold Counter Operators. The threshold counter operator with threshold value n is

where T consists of the transformations inc and id, with inc(x) = x + 1; the function ϕ is defined as ϕ(1) = inc and ϕ(0) = id; and the function ψ is defined as ψ(x) = 1 if x ≥ n and ψ(x) = 0 otherwise. The operator allows one to check whether a given condition has occurred at least n times. Notably, we can define the operator equivalently as a finite operator by replacing the set of all natural numbers N with the finite set [0, n] and modifying the increment transformation as inc(x) = min(n, x + 1). They are equivalent because ψ will not distinguish integers greater than n.

Example 3. An agent must collect at least 30 units of stone, and at least 115 units of iron given that 13 have already been collected. When it has collected a sufficient number of units, it can deliver and get rewarded. The reward function is described by the query (P, reward) where P consists of the following definitions:

enoughStone :=T30(stone | 0),

successfulDelivery :=enoughStone ∧ enoughIron

alreadyDelivered := successfulDelivery,

notAlreadyDelivered :=¬alreadyDelivered,

reward :=delivery ∧ notAlreadyDelivered.

The proposition reward holds true at the first time point when the agent succeeds in a delivery.

Parity Operator. The parity operator is

where T consists of the identity function id and the Boolean negation function ¬; and the function ϕ is defined as ϕ(0) = id and ϕ(1) = ¬. The operator checks whether the input variable has been true an even number of times. It is exemplified by the program

which defines whether a has happened an even or odd number of times.

Metric Temporal Operators. In the style of metric temporal logic [Koymans, 1990], we can define operators such as one that checks whether something happened in the last k steps-with time isomorphic to the naturals rather than to the reals as in the original metric temporal logic. The aforementioned operator is defined as

where the set T has transformations set and dec defined as set(x) = k and dec(x) = x - 1; the function ϕ is defined as ϕ(1) = set and ϕ(0) = dec; and the function ψ is defined as ψ(x) = 1 if x > 0 and ψ(x) = 0 otherwise. The operator can be equivalently defined as a finite operator by replacing Z with [0, k], and definining dec(x) = max(0, x - 1).

Operators with infinite transformation domain. While all the operators above can be defined as finite operators, one can also include operators that require an infinite transformation domain. For instance, the operator

where T consists of inc(x) = x + 1, id(x) = x, and dec(x) = x - 1; the function ϕ is defined as ϕ(0, 0) = ϕ(1, 1) = id, ϕ(1, 0) = inc, ϕ(0, 1) = dec; and the function ψ is defined as ψ(x) = 1 iff x = 0. When the operator is used in a definition such as

we have that variable p is true iff a and b have been true the same number of times. The operator can be used to recognise the Dyck language of balanced parentheses, which is not regular. The existence of an equivalent finite operator would imply the existence of a finite automaton, and hence regularity of the language.

3.2 Finite Semigrouplike Operators

We present a principled way to define operators in terms of finite semigroups.

Definition 1. Let us consider a finite semigroup S = (X, · ), a surjective function ϕ : Bm → X, and an injective function ψ : X → Bn . They define the transformation operator ⟨X, T, ϕ, ψ⟩ where T consists of each transformation y(x) = x · y for y ∈ X. We call it a semigrouplike operator.

Intuitively, ϕ is a binary decoding of the set X, and ψ is a binary encoding. Note that y is seen both as an element of X and as a function y : X → X. From now on we assume that for every set X such an encoding and decoding is fixed. Any choice will be valid for our purposes. Thus, we simply say that a semigroup defines a semigrouplike operator, without mentioning the functions ϕ and ψ explicitly.

Definition 2 (Prime operators). The flip-flop operator is the transformation operator defined by the flip-flop monoid. An operator is a (simple) group operator if it is defined by a (simple) finite group. The prime operators are the flip-flop operator and the simple group operators.

We will focus in particular on the flip-flop operator and on operators defined by cyclic groups. For these two operators we provide an explicit definition, which requires us to commit to a choice of the encoding/decoding functions. The definitions we provide are improved with respect to the ones following from a direct application of Definition 1. In particular, we omit one element from the transformation domain of the flip-flop operator, since it would be redundant.

Definition 3. The flip-flop operator is

where T consists of the transformations set, reset, read defined as

and the function ϕ is defined as

The flip-flop operator corresponds to the flip-flop from digital circuits-it corresponds to an SR latch, where input 11 is not allowed though, cf. [Roth et al., 2004]. The operator allows us to specify a flip-flop with a definition as

Therefore the logic L(F) can be employed as a specification language for digital circuits with logic gates and flip-flops. Next we introduce the cyclic operators.

Definition 4. The cyclic operator of order n is

where the transformations are T = {inci | i ∈ [0, n - 1]} defined as

the function ϕ is defined as

where m is the minimum number of bits required to represent n, and i is the minimum between n-1 and the number whose binary representation is b1 . . . bm; finally, the function ψ(x) yields the binary representation of x.

When a cyclic operator is used in a definition as

variables p1, . . . , pm provide the binary representation of the number of times a has been true modulo n. Note that the parity operator introduced earlier coincides with C2. Next we characterise the prime cyclic operators.

Proposition 1. A cyclic operator Cn is a prime operator iff n is a prime number.

The other prime operators are defined by finite simple groups as found in the classification of finite simple groups, cf. [Gorenstein et al., 2018]. In addition to the infinite family of cyclic groups of prime order, the classification also includes the two infinite families of alternating groups and groups of Lie type, along with the 27 sporadic groups.

4 Expressivity Results

We show expressivity results for Transformation Logics featuring finite operators, with a focus on semigroup-like operators. We start by defining the notion of expressivity for a Transformation Logic, in terms of formal languages.

Definition 5. Consider a program P with input variables V = {p1, . . . , pn}. Every letter ⟨b1, . . . , bn⟩ of the alphabet Bn defines an assignment ν to the variables in V , as ν(pi) = bi. Then, every word w over Bn defines an input Iw to P. A query (P, q) accepts a word w over Bn iff (P, Iw, |w|) |= q; and it recognises a language L over Bn if it accepts exactly the words in L.

Definition 6. The expressivity of a logic L is the set of languages recognised by its queries. A logic L1 is less expressive than a logic L2, written L1 ⊏ L2, if the expressivity of L1 is properly included in the expressivity of L2.

First, we establish the expressivity when all finite operators are included.

Theorem 1. For A the set of all finite operators, the expressivity of L(A) is the regular languages.

The result follows from the fact that finite operators capture finite automata; conversely, programs with finite operators can be mapped to a composition of finite automata. In particular to a so-called cascade composition of automata. This characterisation allows us to employ algebraic automata theory, cf. [Ginzburg, 1968; Arbib, 1969; D¨om¨osi and Nehaniv, 2005], in proving that prime operators suffice to capture regular languages.

Theorem 2. For P the set of all prime operators, the expressivity of the logic L(P) is the regular languages.

The result is obtained by showing that every transformation definition with a finite transformation operator can be captured by a program with prime operators only. The prime operators to use are suggested by the prime decomposition theorem for finite automata [Krohn and Rhodes, 1965]. For starfree regular languages, we obtain the following specialised result.

Theorem 3. For F the flip-flop operator, the expressivity of the logic L(F) is the star-free regular languages.

Beyond star-free, we have nameless fragments of the regular languages. Here we start their exploration. First, to go beyond star-free it suffices to introduce group operators.

Theorem 4. For any non-empty set G of group operators, the logic L(F,G) is strictly more expressive than L(F).

Next we focus on cyclic operators. We show them to yield a core of the Transformation Logics with favourable properties. First, cyclic operators along with the flip-flop operator form a canonical and universal set of operators for the logic L(F, S), where S is the set of all solvable group operators. They are canonical and universal for L(F, S) in the same way the operators {∧, ¬} are canonical and universal for propositional logic. We state universality and then canonicity.

Theorem 5 (Universality). For C the set of all cyclic operators of prime order, and S any set of solvable operators, the expressivity of L(F, C) includes the expressivity of L(F, S).

Theorem 6 (Canonicity). Given two sets C1 and C2 of cyclic operators of prime order, the logics L(F,C1) and L(F,C2) have the same expressivity if and only if C1 = C2.

The canonicity result implies the existence of infinite expressivity hierarchies such as the following one, if we note that every Cp is a prime operator when p is a prime number.

It is worth noting that this form of canonicity does not hold for prime operators in general.

Theorem 7. There are two sets P1 ⊂ P2 of prime operators such that L(P1) and L(P2) have the same expressivity.

Combining our expressivity results together, we obtain the following hierarchy theorem.

Theorem 8. For S all solvable group operators, and P all prime operators, the following infinite hierarchy of expressivity holds:

The theorem provides our current picture of the expressivity of the Transformation Logics. At the bottom of the hierarchy we have L(F) with the expressivity of the star-free regular languages. At the top of the hierarchy we have L(P) with the expressivity of all regular languages. Between them we have infinitely-many logics capturing distinct fragments of the regular languages.

5 Complexity Results

We study the complexity of the evaluation problem for the Transformation Logics.

Definition 7. The evaluation problem of a Transformation Logic L is the problem to decide, given a query (P, q) with P ∈ L, and an input I = I1, . . . , Iℓ for P, whether it holds that (P, I, ℓ) |= q.

To study the complexity we need to assume a representation for the operators, which determines the size of an operator. The choice of a representation for operators in general is beyond the scope of this paper. We discuss two concrete cases below.

Definition 8. A family T of operators is polytime if, for every operator ⟨X, T, ϕ, ψ⟩ ∈ T with ϕ : Bm → T and ψ : X → Bn , it holds that, for every x ∈ X and every µ ∈ Bm, the value ψ(τ(x)) with τ = ϕ(µ) can be computed in time polynomial in the size of the operator.

Theorem 9. For any (possibly infinite) set T of polytime operators, the evaluation problem of L(T) is in PTIME. Furthermore, there exists a set H of polytime operators such that the evaluation problem of L(H) is PTIME-complete.

We argue the upper bound applies to every finite set of finite operators, including prime operators. On the contrary, infinite sets of finite operators may not be polytime.

Lemma 1. Every finite set of finite operators is polytime. There exists a set of finite operators that is not polytime.

Theorem 10. For any finite set T of finite operators, the evaluation problem of L(T) is in PTIME.

Next we focus on threshold counter operators Tn and cyclic operators Cn. We denote the complete families as {Tn} and {Cn}. Notably, such operators can be represented compactly.

Definition 9. A representation for the family of threshold counter operators {Tn} is said to be compact if the size of the representation of Tn is O(logn). Similarly for the family of cyclic operators {Cn}.

A compact representation can be obtained by encoding the symbols T and C with a constant number of bits, and the index n in binary with a logarithmic number of bits.

Proposition 2. The threshold-counter operators {Tn} and the cyclic operators {Cn} admit a compact representation.

Lemma 2. The families of operators {Tn} and {Cn} are polytime, even when represented compactly.

Overall we obtain that polynomial time evaluation is possible for every Transformation Logic that includes any finite number of finite operators, along with the threshold-counter and cyclic operators.

Theorem 11. For any finite set A of finite operators, the evaluation problem of L(A, {Tn}, {Cn}) is in PTIME even under compact representation of the operators {Tn} and {Cn}.

5.1 Constant-Depth and Data Complexity

We study the complexity of evaluation of programs having a constant depth. It implies data complexity results. Specifically, all membership complexity results for constant-depth programs imply also membership in data complexity, when the program is fixed and the size of the input to the program is arbitrary. Data complexity measures how evaluation of a fixed program scales with the size of the input [Vardi, 1982]. We first define the depth of a program, and corresponding classes of constant-depth programs.

Definition 10. Consider a program P . The depth of an input variable of P is zero. The depth of a variable defined by a static definition d ∈ P is the maximum depth of a variable in the body of d plus the depth of the parse-tree of the body of d. The depth of a variable defined by a delay or transformation definition d ∈ P is the maximum depth of a variable in the body of d plus one. The depth of P is the maximum depth of a variable in P .

Definition 11. For any set of transformation operators T, and any depth k, the Transformation Logic L(T| k) is the subset of L(T) with programs of depth at most k.

Our results are phrased in terms of three circuit complexity classes, reported below with the known inclusions.

The first result is for the flip-flop operator, and it builds on a result for the complexity of group-free semigroups [Chandra et al., 1985].

Theorem 12. For any k, evaluation of L(F | k) is in AC0 .

Cyclic group operators, and solvable group operators in general, increase the complexity of the evaluation problem.

Theorem 13. For any depth k, and any finite set S of solvable group operators, evaluation of L(F, S | k) is in ACC0 . Furhermore, there is a solvable group operator G such that, for every depth k ≥ 1, evaluation of L(G | k) is not in AC0 .

The upper bound makes use of a result for the complexity of solvable groups [Barrington, 1989]. The lower bound relies on the fact that the cyclic (hence solvable) group C2 captures the parity function, known not to be in AC0 [Furst et al., 1984].

Non-solvable groups introduce an exact correspondence with the larger cicuit complexity class NC1 . Our result builds on a result for the complexity of non-solvable groups [Barrington, 1989].

Theorem 14. For any depth k, and any finite set G of groups containing a non-solvable group, the evaluation problem of L(F,G| k) is complete for NC1 under AC0 reductions.

6 Relationship with Past LTL

We show the Transformation Logic L(F) captures Past LTL. First, the before and since operators correspond to the delay and flip-flop operators, respectively.

Lemma 3. Consider a Past LTL formula φ = p. Let P be the singleton program consisting of the definition q := Dp. For every interpretation I of φ and every time point t, it holds that (I, t) |= φ iff (P, I, t) |= q.

Lemma 4. Consider a Past LTL formula φ = aS b. Let P be the program consisting of the two definitions c := ¬a and p := F(b, c | 0). For every interpretation I of φ and every time point t, it holds that (I, t) |= φ iff (P, I, t) |= p.

Given the lemmas above, we can build a program for any given Past LTL formula by induction on its parse-tree, introducing one static definition for each occurence of a Boolean operator, one delay definition for each occurrence of the before operator, and one transformation definition for each occurrence of the since operator.

Theorem 15. Every Past LTL formula φ can be translated into a program of L(F). Such a program has size linear in the size of φ, and it can computed from φ in logarithmic space.

7 RelatedWork

The Transformation Logics are a valuable addition to the rich set of temporal and dynamic logics adopted in AI. Such logics include propositional temporal logics of the past such as Past LTL, cf. [Manna and Pnueli, 1991]; temporal logics of the future interpreted both on finite and infinite traces [Pnueli, 1977; Wolper, 1983; De Giacomo and Vardi, 2013]; dynamic logics such as PDL, cf. [Harel et al., 2000], and linear dynamic logic on finite traces [De Giacomo and Vardi, 2013]; logics with a dense interpretation of time such as metric temporal logic [Koymans, 1990]. They also include first-order variants such as Past FOTL [Chomicki, 1995]. Finally, they include rule-based logics of several kinds: propositional modal temporal logics such as Templog [Abadi and Manna, 1989; Baudinet, 1995]; logics with first-order variables where time occurs explicitly as an argument of a special sort such as Datalog1S [Chomicki and Imielinski, 1988], and Temporal Datalog [Ronca et al., 2018; Ronca et al., 2022]; logics with metric temporal operators such as DatalogMTL [Brandt et al., 2018; Walega et al., 2019; Walega et al., 2020]; and propositional modal logics specialised for reasoning on streams [Beck et al., 2018], and weighted variants thereof [Eiter and Kiesel, 2020] which share an algebraic flavour with our work.

8 Conclusions

The Transformation Logics provide a general framework for logics over sequences. The flexibility given by the transformation operators allows for defining logics with the expressivity of many different fragments of the regular languages, under the guidance of group theory. While the star-free regular languages are well-known as they are the expressivity of many well-established formalisms, the fragments beyond them are less known. The Transformation Logics provide a way to explore them.

Acknowledgments

Alessandro Ronca is supported by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT). For the purpose of Open Access, the author has applied a CC BY public copyright licence to any Author Accepted Manuscript (AAM) version arising from this submission.