2 Temporal logics at a glance

Linear-time temporal logics define temporal models as sequences of states. Following common conventions in AI (De Giacomo and Vardi Reference De Giacomo and Vardi2013), we restrict our focus to finite sequences of states, which serve as the core semantic foundation for the temporal ASP extensions considered in this work. Standard linear-time logics (Pnueli Reference Pnueli1977) incorporate temporal modal operators, such as next ( ${\huge \circ}$ ), always ( $\square$ ), and eventually ( $\Diamond$ ). Specifically, ${\huge \circ} \varphi$ requires that $\varphi$ holds in the immediate successor state, while $\square \varphi$ and $\Diamond \varphi$ demand that $\varphi$ holds in all or some future states (including the current one), respectively. Furthermore, we utilize the initial-state operator $\boldsymbol{\mathsf{I}}$ , which holds exclusively in the first state of a sequence. Additional operators can be derived from these primitives; for example, the final-state operator $\boldsymbol{\mathsf{F}}\equiv \neg {\huge \circ} \top$ only holds at the terminal state of a finite sequence. More formally, a temporal model $(X_i)_{i=0}^{n}$ , consisting of a sequence of $n{+}1$ interpretations, satisfies a formula formed with our example operators at time step $t\in \{0,\dots ,n\}$ , if

(1) \begin{align} (X_i)_{i=0}^{n}, t \models \boldsymbol{\mathsf{I}} \quad & \text{ iff } t =0, \end{align}

(2) \begin{align} (X_i)_{i=0}^{n}, t \models {\huge \circ} \varphi & \text{ iff } t\lt n \text{ and } (X_i)_{i=0}^{n}, t{+}1 \models \varphi , \end{align}

(3) \begin{align} (X_i)_{i=0}^{n}, t \models \Diamond \varphi & \text{ iff } (X_i)_{i=0}^{n}, j \models \varphi \text{ for some } j\in \{t,\dots ,n\}. \end{align}

In dynamic logic (Pratt Reference Pratt1976), the modal operators $\square$ and $\Diamond$ are parametrized by regular expressions that define paths over sequences of states. Specifically, the dynamic formulas $[\rho ]\,\varphi$ and $\langle \rho \rangle \,\varphi$ require that $\varphi$ holds in all or some of the states, respectively, reachable via a path segment satisfying the expression $\rho$ . Similarly, in metric temporal logic (Alur and Henzinger Reference Alur and Henzinger1992), $\square$ and $\Diamond$ are parametrized by a time interval, which, in our context, is defined over natural numbers. The metric formulas $\square _{[l..u)}\varphi$ and $\Diamond _{[l..u)}\varphi$ stipulate that $\varphi$ holds in all or some states, respectively, whose associated time point lies within the interval $[t{+}l..t{+}u)$ , where $t$ denotes the current time point.

While these semantic intuitions have been extensively explored across various logical contexts, our work centers on adapting them to the non-monotonic realm of Equilibrium Logics. In particular, we target fragments of $\textrm {TEL}$ , $\textrm {MEL}$ , and $\textrm {DEL}$ that are amenable to implementation via ASP. To bridge this theoretical foundation with a practical implementation, we now establish the semantic infrastructure required to represent discrete state sequences within clingo’s meta-programming framework.

3 Setting the stage for temporal meta-programming

To capture the series of states in linear temporal models, we present in Listing 1 a meta-encoding that extends the one for plain ASP outlined in (Kaminski et al. Reference Kaminski, Romero, Schaub and Wanko2023). This extension relies on a time index provided by the atom time(T) and the inclusion of the variable T as the final argument in the encoding’s primary predicates. The set of instantiated rules sharing a common time index effectively duplicates the behavior of the plain ASP meta-encoding. The number of duplicated ASP encodings is given by the parameter n; see Line 1.

Listing 1.

Timed meta-encoding (teta.lp)

Prior to detailing the encoding in Listing 1, we must establish the underlying reified fact format. For instance, clingo’s reification transforms the (non-temporal) rule

into the following set of facts (omitting definitions for green(l1) and light(l1)):

The syntactic structure of the rule is captured by the reified facts in Lines 1–3. The primary structure is defined by the instance of rule/2 in Line 1, which specifies a disjunctive head and a normal body, both identified by the constant 0. In this format, clingo represents heads and bodies as tuples of atoms and literals, respectively, utilizing the predicates atom_tuple and literal_tuple. Within these tuples, ground literals are mapped to unique integer identifiers. For instance, the rule’s head consists of a single atom represented in Line 2 as the tuple (3), while the body is represented in Line 3 as a conjunction of two literals forming the tuple (-2,1). Finally, the output/2 facts in Lines 4–6 establish the necessary mapping between human-readable symbolic names and these internal integer identifiers. For example, output(light(l1),1) links the symbolic atom to the integer 1 via the corresponding literal tuple (1).Footnote ²

Notably, clingo’s reification process is subject to stable-models-preserving simplifications that occur during grounding. Consequently, the resulting set of reified facts reflects the simplified rule structure rather than the original program. If the truth value of a body literal is established during the grounding phase, that literal is removed from the rule and, by extension, from its reified representation. For instance, this occurs if a negative literal “not green(l1)” is satisfied because green(l1) is non-derivable. Conversely, if a rule’s body is determined to be unsatisfiable, the entire rule becomes vacuous and is eliminated, along with its associated reified facts. This scenario arises, for example, if “not green(l1)” is found to be false because green(l1) has been established as true.

Following the reification of the original program, the resulting facts are combined with a meta-encoding and processed by an ASP system. In the meta-encoding presented in Listing 1, the truth of a literal at a specific time step is represented by instances of the hold/2 predicate. Accordingly, the rule in Lines 3–5 derives an instance of conjunction(B,T) for a time step T, if all literals within the associated literal_tuple(B) hold at that time. This enables the derivation of body(normal(B),T) in Line 7 whenever the literal tuple B represents a normal rule body. Consequently, the head atoms of the corresponding rule are derived in Lines 13 or 13. For instance, using our previous example facts and assuming that we have time(0) and hold(1,0) but not hold(2,0), we derive conjunction(0,0) and body(normal(0),0), ultimately concluding hold(3,0) via the rule in Line 12. For a comprehensive account of clingo’s reification, we refer to (Kaminski et al. Reference Kaminski, Romero, Schaub and Wanko2023).

Thus far, our meta-encoding captures the program’s behavior at each time step independently, effectively yielding a sequence of isolated state valuations. In the following, we describe how temporal operators are utilized to establish the necessary logical connections between these states, thereby defining the resulting temporal stable models.

4 Temporal meta-programming

To illustrate our approach, we consider a traffic light system modeled with linear-time temporal operators in (4) to (6). In this scenario, a traffic light is red by default, unless it is green. When a pedestrian button is pushed, the light becomes eventually green from the next step on. The button for light $\mathit{l_1}$ is pushed one step after the initial state.

(4) \begin{align} \square ( \neg \mathit{\mathit{green}(L)} \to \mathit{\mathit{red}(L)} ) \end{align}

(5) \begin{align} \square ( \mathit{push(L)} \to {\huge \circ} {\Diamond \mathit{green(L)}} ) \end{align}

(6) \begin{align} {\huge \circ} {\mathit{push(\mathit{l_1})}} \end{align}

In $\textrm {TEL}$ , these constraints yield no temporal models of length one and two, but one of length three, given by the state sequence: $ \langle \{\mathit{red}(\mathit{l_1})\}, \{\mathit{red}(\mathit{l_1}),\mathit{push(\mathit{l_1})}\}, \{\mathit{green(\mathit{l_1})}\} \rangle$ .

Listing 2.

Abridged linear-time temporal grammar (tel-grammar.lp).

4.1 Syntax definition

To define the additional syntax required for temporal expressions, we extend the theory language of clingo by #type definitions.Footnote ³ A representative grammar for the type tel is given in Listing 2, which serves to augment standard clingo atoms with temporal formulas whose arguments remain regular clingo terms. This extension is facilitated by the subtypes field in Line 2, permitting the inclusion of other types, such as the predefined type atom for standard clingo atoms, into our temporal expressions. Consequently, a standard atom like green(l1) is treated as a tel expression and functions as a valid argument of type tel within nested temporal formulas. Other supported base types include number, string, infimum, and supremum.

Lines 3–8 define the formation of temporal expressions incorporating the $\top$ , $\neg$ , $\boldsymbol{\mathsf{I}}$ , ${\huge \circ}$ , $\Diamond$ , and $\boldsymbol{\mathsf{F}}$ operators, each prefixed by amp in accordance with clingo’s theory grammar conventions. To support nesting, the specification is defined recursively, allowing constructs such as & true or & not (Line 3) to be embedded within other expressions. This recursive design facilitates the customization of existing constructs and enables the seamless addition of new operators, such as a Boolean & or. Unlike standard theory atoms, these temporal formulas can be nested and utilized within conditional literals or aggregates. For example, the conditional “ & eventually(green(L)) : light(L)” concisely stipulates that “every light must eventually turn green.” Expressions are further refined by specifying the type and the safety condition for their arguments, which are essential for subsequent transformations. For instance, the arguments for & next and & eventually are of type tel and are declared as safe, whereas the argument for & not is declared as unsafe. Indeed, the latter declaration can be omitted, as unspecified safety conditions default to unsafe.

Defined operators can be specified with macros. In Line 8, for example, we define the final-state operator $\boldsymbol{\mathsf{F}}$ as $\neg {\huge \circ} \top$ , which motivates the inclusion of & true and & not in the base specification. For more complex operators with arguments, placeholders can be used, as detailed in Section 5 and 6. Furthermore, the occurrence keyword identifies the valid syntactic positions for expressions of a given type, namely any, head, body, or directive. While tel expressions are permitted in both heads and bodies of rules (any), omitting this declaration restricts a type to serving exclusively as an argument for other expressions. This distinction is essential for defining auxiliary types, like intervals in Section 5, which act as structural components rather than standalone atoms.

Using the grammar in Listing 2, we can express the rules in (4) to (6) as in Listing 3. For simplicity, each rule is implicitly governed by the “always” operator $\square$ , meaning it applies at every time step of the temporal model. Rules restricted to the initial state, like (6), are qualified by the & initial operator (representing $\boldsymbol{\mathsf{I}}$ ) within their body to anchor them to the first state of the model.

Listing 3.

Linear-time temporal example (telex.lp).

4.2 Non-ground transformations

Logic programs containing type expressions undergo several transformations to leverage standard grounding technology without compromising semantic correctness. The initial phase converts programs with temporal type expressions into standard programs parsable by clingo. This transformation is designed to be partially reversible during output processing to maintain readability.

The primary objective of our non-ground transformations is to avoid incorrect simplifications during grounding. To achieve this, the system instruments the input program with #external statements. As illustrated in Listing 4, a directive such as “#external push(l1).” in Line 8 instructs the grounder to exempt that specific atom from simplifications. Without this protection, the grounder would erroneously assume that expressions like & initial or instances of push/1 and green/1 are non-derivable and therefore false. This would lead to semantically incorrect models, such as a traffic light remaining red indefinitely.

Listing 4.

Result of (non-ground) transformation of Listing 3.

The generation of these protective directives relies on an extended definition of safety. An atom occurrence in a rule body is deemed safe, if it is neither within the scope of negation nor within the scope of an argument of a theory expression declared as unsafe in the grammar. A rule is considered safe if all its variables occur in safe body atoms. For example, the rule “wait(L) :- &eventually(green(L)), not green(L).” is safe because the variable L is bound by the occurrence of green(L) within the first conjunct. This occurrence is safe because the single argument of & eventually/1 is declared as safe in the grammar and is not negated. Conversely, if a variable only appears within negated literals, such as “not green(L),” or within theory expressions declared as unsafe (e.g., & not(green(L))), the rule is deemed unsafe.

In our system, safety verification is interleaved with the generation of external directives. For each safe rule, metasp generates two distinct types of #external. The first type prevents the grounder from discarding rules with body expressions that might be deemed non-derivable. The system adds one #external statement for each temporal expression in the body, conditioned by the rule’s safe body atoms to ensure correct variable binding. For instance, our wait example yields “#external &eventually(green(L)): green(L).” Similarly, the statement in Line 7 is induced by the rule in Line 4. The second type ensures that atoms within head expressions are explicitly incorporated into the grounder’s instantiation domain. The system generates an #external directive for every atom appearing within a non-negated head expression, again conditioned on safe body atoms to maintain correct variable bindings. As illustrated in Line 6 of Listing 4, this ensures that atoms like green(L) remain part of the grounding domain even when nested within modalities like & eventually. This incorporation of #external directives allows for a complete ground instantiation in a single call to clingo, representing a significant advancement over previous two-pass temporal grounding methods (Cabalar et al. Reference Cabalar, Pearce and Valverde2010); its formal correctness is established in (Nemes Reference Nemes2024).

Declaring safety conditions for expression arguments is critical to theory grammar design. A sufficient criterion is whether the satisfaction of a formula implies the satisfaction of its argument at some time step. In $\textrm {TEL}$ , the arguments of & next/1 and & eventually/1 meet this criterion and are thus declared safe. When this fails, the argument is better declared unsafe. For instance, Nemes (Reference Nemes2024) shows that the single arguments of $\circ$ , $\Diamond$ , and $\Box$ provide safe bindings in $\textrm {TEL}$ (as do the second arguments of “until” and “release”).Footnote ⁴

Finally, #show directives are transformed into internal rules and subsequently reified. This process provides a comprehensive symbol table, expressed through output/2 facts, and yields specialized facts such as show_atom/2 and show_term/2 that capture the syntactic conditions of the original directives. By leveraging these reified statements, users can define declarative output policies to customize the output of complex temporal formulas. We refer the reader to (Hahn et al. Reference Hahn, Nemes, Romero and Schaub2026) for a detailed account of this mechanism.

4.3 Extended reification

Once non-ground transformations are complete, the program is grounded and reified using an extension of clingo’s reification process designed for temporal formulas. During this phase, type checking and operator expansion are interleaved with grounding, allowing the system to record each subformula and its associated type through corresponding formula/2 facts. In our example, the resulting subformulas are detailed in Lines 6–13 of Listing 5; for instance, Lines 9–11 represent the reified subexpressions derived from & next( & eventually(green(l1))). Notably, a single subformula may appear in multiple formula/2 facts, depending on its type memberships. For example, green(l1) is simultaneously categorized as an atom and a temporal expression (tel). The formula/2 predicate serves as a domain predicate in our meta-encodings, effectively constraining the instantiation of formula-based rules. This representation allows us to easily incorporate advanced syntactic concepts, such as the closure of Fischer and Ladner (Reference Fischer and Ladner1979) in Section 6, by simply adding auxiliary rules to define extended subexpression relationships.

Listing 5.

Reified temporal example.

Standard symbol table information is retained via the output/2 predicate. Because our non-ground transformations instrument the program by inserting #external directives and removing #show statements, the grounder is prevented from aggressively simplifying the program, and all atoms and temporal formulas are preserved as output/2 facts. The symbol table obtained in our example is given in Lines 1–4 of Listing 5.

The core of this reified representation utilizes standard reification predicates: a rule/2 instance for each rule in the original program is provided alongside the associated atom_tuple and literal_tuple facts that capture their respective heads and bodies as outlined in Section 3. In addition to the output/2 and formula/2 facts, the representation incorporates external/2 facts, as well as show_term/2 and show_atom/2 instances. These correspond to the injected #external directives and transformed #show statements. For the sake of brevity, these specific predicate instances are omitted from the discussion.

4.4 Temporal meta-encoding

A meta-encoding operationalizes the semantics of a logic program by defining the underlying semantic structure and interpreting the program’s components within that structure. The design of our meta-encoding reflects this bipartite nature: the first part (Listing 1) establishes a sequence of independent stable models, where temporal formulas are treated as standard atoms, while the second (Listing 6) accounts for the satisfaction relation of temporal operators $\boldsymbol{\mathsf{I}}$ , ${\huge \circ}$ , and $\Diamond$ .

The first part of our meta-encoding employs the predicate hold/2 to represent the valuation of literals along different time steps; this representation captures linear-time temporal models and is thus common to the temporal logics $\textrm {TEL}$ , $\textrm {MEL}$ , and $\textrm {DEL}$ .

The transition between both parts relies on the true/2 predicate. While hold/2 refers to atoms and formulas via numeric identifiers, true/2 utilizes their symbolic representations. This distinction is vital, as it enables the evaluation of operators based on their inherent syntactic structure rather than opaque identifiers. To this end, the hold/2 atoms are related to nested temporal formulas through the true/2 predicate in Listing 6 to capture the inductive definition of satisfaction. The rules in Lines 1–2 establish the base case by synchronizing hold/2 and true/2 instances for all elements in the symbol table. Whenever a symbolic representation o corresponds to a numeric identifier l, the system typically relies on the presence of the facts output(o,b) and literal_tuple(b,l) to enforce the equivalence between true(o,t) and hold(l,t) along all time steps t. However, a subtle distinction arises when a formula o appears as a fact: because it lacks an associated rule body, the corresponding literal_tuple/2 is absent from the reified output. This is elegantly handled by the rule in Line 1 via a conditional, which allows for deriving true(o,t) directly from the symbol table, while the first part of the meta-encoding independently establishes the truth of the corresponding fact hold(l,t).

Listing 6.

Encoding of $\textrm {TEL}$ semantics of $\boldsymbol{\mathsf{I}}$ , ${\huge \circ}$ , and $\Diamond$ (tel-semantics.lp).

Building on this, the satisfaction relations for $\boldsymbol{\mathsf{I}}$ , ${\huge \circ}$ , and $\Diamond$ are implemented by the subsequent rules in Listing 6. The individual cases, and thus the overall grounding process, is governed by formula/2, acting as a domain predicate. Each group of rules in Lines 4–5, 7–9, and 11–13 establishes a logical equivalence that captures the formal truth conditions for $\boldsymbol{\mathsf{I}}$ , ${\huge \circ}$ , and $\Diamond$ as defined in (1), (2), and (3), respectively. For instance, the satisfaction of $\Diamond \varphi$ in (3) can be expressed in our framework as true( & eventually(F),T) iff true(F,j) for some $\mathtt {j} \in \{\mathtt {T},\dots ,\mathtt {n}\}$ . This bidirectional relationship is realized in Lines 11 and 13, whose rules collectively enforce the semantics of the “eventually” operator.

Taken together, the theory grammar in Listing 2 and the meta-encodings in Listing 1 and 6 provide a complete framework for evaluating our temporal program presented in Listing 3. More generally, given a temporal logic program $P$ , and $n\geq 0$ , we get a 1–1 correspondence between the temporal models of length $n$ of $P$ and the stable models of the reification of $P$ , obtained using Listing 2, together with Listings 1 and 6. The broader functionality of our tool, metasp, is discussed in Section 7.

5 Metric meta-programming

Having established our meta-programming workflow through $\textrm {TEL}$ , we now demonstrate the framework’s extensibility within the more complex setting of $\textrm {MEL}$ . This section illustrates how our approach handles quantitative temporal constraints by leveraging a modular grammar and hybrid solving techniques.

The grammar for this metric extension, detailed in Listing 7, incorporates the auxiliary types interval and ub to facilitate the representation of temporal intervals. Intervals are constructed using the binary operator & i, which pairs a numeric lower bound with an upper bound of type ub (Line 2). As specified in Line 1, this upper bound may be either a specific number or the constant #sup, the sole member of the predefined supremum type. Both types are predefined in metasp and serve purely as structural components. In fact, while expressions of type mel are permitted to occur in rule heads and bodies (as declared in Line 11), the interval and ub types are restricted from appearing as standalone atoms. This is enforced by the absence of an occurrence declaration for these types. Furthermore, both arguments of the interval operator & i are considered unsafe, as reflected by the lack of explicit safety declarations in the grammar.

Listing 7.

Abridged metric temporal grammar.

Following the pattern of $\textrm {TEL}$ expressions, Line 5 to 8 define formulas involving expressions with $\boldsymbol{\mathsf{I}}$ , ${\huge \circ} _{[l..u)}\varphi$ , and $\Diamond _{[l..u)}\varphi$ . The latter two are captured by the binary operators next/2 and eventually/2, which pair a metric interval with a mel formula. Similar to $\textrm {TEL}$ , the second argument of type mel is considered safe, while the first, interval argument is declared unsafe. To streamline the syntax, Line 10 introduces a unary variant of the & next operator representing the unconstrained metric operator ${\huge \circ} _{[0..\omega )}$ . In this context, the interval imposes no constraints, and the operator amounts to its qualitative counterpart ${\huge \circ}$ in $\textrm {TEL}$ . This allows us to write & next(F) as a shorthand for the more verbose & next( & i(0,#sup),F), where F is a mel formula. To facilitate this in the theory specification, placeholders are utilized; these are specific constants that are declared and assigned types within a where clause.

The metric counterpart of our traffic lights example is provided in Listing 8. This encoding differs from Listing 3 primarily in Line 3, where the plain eventually head atom is replaced by its metric counterpart & eventually( & i(10,15),green(L)), stipulating that the light must turn green between time points 10 and 15. The occurrence of & next(push(l1)) in Line 4 is replaced during reification by & next( & i(0,#sup),push(l1)).

Listing 8.

Metric temporal example.

To accommodate $\textrm {MEL}$ ’s dual nature, combining qualitative temporal progression with quantitative timing constraints, our meta-encoding utilizes the hybrid ASP solver clingcon (Banbara et al. Reference Banbara, Kaufmann, Ostrowski and Schaub2017) to leverage its native support for linear constraints over integers. Formally, each state $X_t$ in a temporal model $(X_i)_{i=0}^{n}$ is associated in $\textrm {MEL}$ (Becker et al. Reference Becker, Cabalar, Diéguez, Hahn, Romero and Schaub2024b) with a discrete time point via a timing function $\tau$ satisfying $\tau (0) = 0$ and $\tau (t) - \tau (t-1) \geq 1$ for $t \in \{1,\ldots ,n\}$ . This relationship is operationalized in Listing 9 using clingcon’s & sum theory atom, in which each instance of functor t/1 takes a non-negative integer value corresponding to a specific time point.

Listing 9.

Encoding of the timing function $\tau$ .

We illustrate the meta-encoding of metric operators in terms of the metric next ${\huge \circ} _{[l..u)}$ . As with $\textrm {TEL}$ , the encoding is derived from semantic principles: A temporal model $(X_i)_{i=0}^{n}$ with a timing function $\tau$ satisfies ${\huge \circ} _{[l..u)} \varphi$ at time step $t\in \{0,\dots ,n\}$ , written $ (X_i)_{i=0}^{n}, t \models {\huge \circ} _{[l..u)} \varphi$ , if

\begin{align*} (X_i)_{i=0}^{n}, t{+}1 \models \varphi \text{ and } \tau (t+1)-\tau (t)\in [l..u) \text{ for } t\lt n \ . \end{align*}

We can express this within our framework as: true(&next(&i(L,U),F),T) iff true(F,T + 1), &sum t(T + 1); −t(T) >= L, &sum t(T + 1); −t(T) <U, and T <n. The right-to-left direction of this equivalence is given in Listing 10. The left-to-right direction is encoded analogously with four rules, one for each conjunct. The full encoding can be found at (Hahn et al. Reference Hahn, Nemes, Romero and Schaub2026).

Listing 10.

Encoding for MEL semantics of ${\huge \circ} _{[l..u)}$ .

6 Dynamic meta-programming

Lastly, we demonstrate the extensibility of our approach through $\textrm {DEL}$ . The grammar for this extension, provided in Listing 11, inherits the $\textrm {TEL}$ type definitions via the subtypes field.Footnote ⁵ Path expressions, defined in Lines 9–15, serve exclusively as arguments for the dynamic modal operators. These paths incorporate standard constructors, such as step ( $\unicode {x03C4}$ ), test ( $?$ ), star ( $*$ ), choice ( $+$ ), and sequence (;), to define regular expressions over state sequences. The macro introduced in Line 15 permits an atom $a$ to be used directly in path expressions by translating it into the expression $(a?;\unicode {x03C4})$ , a replacement strictly confined to the context of path expressions.Footnote ⁶

Listing 11.

Abridged dynamic temporal grammar.

Listing 12.

Additional rules for the Fischer–Ladner closure of &eventually formulas.

For example, the formula $ \boldsymbol{\mathsf{I}}\wedge \langle (\mathit{green(l_1)};\mathit{red(l_1)})^*\rangle \, \boldsymbol{\mathsf{F}}$ describes temporal models where light $l_1$ alternates between green and red. This is expressed in our framework as an integrity constraint:

This constraint effectively utilizes the tel operators & initial and & final alongside the new dynamic constructs. The instances of green(L) and red(L) are expanded during reification into & seq( & test(green(L)), & step) and & seq( & test(red(L)), & step).

In $\textrm {DEL}$ , the satisfaction relation has a scope that extends beyond the subformulas explicitly present in the input. One must also capture the recursive interplay between dynamic modal operators and path expressions, which requires a superset of the subformulas referred to as the Fischer and Ladner (Reference Fischer and Ladner1979) closure. In our framework, this closure is obtained declaratively by extending the definition of the formula/2 predicate, as demonstrated for & eventually in Listing 12. For instance, Line 1 unfolds the “star” operator by one repetition, while Line 4 decomposes a sequence into nested modalities. This declarative expansion of the subformulas ensures that the meta-encoding can verify path satisfaction through a finite set of subexpressions derived entirely via ASP rules. The full encoding can be found at (Hahn et al. Reference Hahn, Nemes, Romero and Schaub2026).

7 The metasp system

The metasp system encapsulates our meta-programming workflow, providing a unified interface for defining and solving temporal ASP extensions. The system is implemented via an Application class that extends the target system’s command line, ensuring full access to native options, such as optimization.

The solve command orchestrates the entire workflow from syntax parsing to model generation. As shown in Listing 13, it requires a target solver, typically clingo, or clingcon for metric extensions, alongside problem-specific and logic-specific encodings.

Listing 13.

System output showcasing the $\textrm {TEL}$ setting.

In Listing 13, we solve our temporal example in file telex.lp (Listing 3) with clingo. The options –syntax-encoding and –semantics-encoding are used to provide the grammar and meta-encodings for the desired logic. Users can customize the output via the –printer option. For example, the built-in temporal_printer organizes atoms by state to improve readability of temporal models. If omitted, the target system’s default printer is used, though users may also provide custom Python scripts for specialized output policies. Standard clingo arguments, such as “-c n = 2” for assigning constant values, are supported directly. The output in Listing 13 reflects a single temporal model, where the light becomes green at state 2, as expected.

To facilitate development, metasp allows users to intercept the transformation process at individual stages: the transform command prints the given program after initial first-order transformations, while reify outputs the extended reification facts. Unlike solve, these diagnostic commands require only grammar definitions and constants, bypassing the need for a back-end solver. For interactive solution exploration, the ui command launches an interface using clinguin (Beiser et al. Reference Beiser, Hahn and Schaub2024). To maintain a clean command-line experience, extension-specific options can be aggregated into configuration files. Finally, metasp supports multiple log levels and issues proactive warnings for common development issues, such as type mismatches or macro redefinitions.

8 Experiments

We conducted an empirical evaluation to assess the performance trade-offs between the flexible meta-programming framework of metasp and the specialized architecture of telingo. Our comparison focuses on $\textrm {TEL}$ and $\textrm {DEL}$ , as these are currently the only temporal extensions supported by telingo. All experiments were conducted on Debian Linux 10 machines with an Intel Xeon E5-2650v4 CPU (2.9 GHz) and 64 GB of RAM. We compare metasp 1.0, utilizing the meta-encodings and grammars partly introduced above with clingo 5.8, against a specialized fork of telingo 2.1.3. Individual runs were constrained by a time limit of 20 min and a memory limit of 24 GB.

Telingo solves $\textrm {TEL}$ and $\textrm {DEL}$ problems incrementally, gradually expanding the horizon. Because our meta-encodings evaluate a fixed horizon, the repeated unsatisfiability checks of the incremental approach would obscure a direct performance comparison. Therefore, we developed telingo- $\lambda$ , a specialized fork of telingo that supports fixed-horizon solving.Footnote ⁷

Figure 1.

Comparison of runtime and solving time of metasp vs telingo- $\lambda$ on $\textrm {TEL}$ problems.

Our $\textrm {TEL}$ evaluation utilizes 69 temporal planning instances from (Cabalar et al. Reference Cabalar, Kaminski, Morkisch and Schaub2019), spanning classic domains: hanoi-towers (red), labyrinth (blue), no-mystery (green), richochet-robots (purple), sokoban (orange), and visitall (brown). The results are visualized in Figure 1, where timeouts for telingo- $\lambda$ and metasp are indicated by upward and rightward arrows, respectively; crosses indicate joint timeouts.

A clear performance trend emerges: on easier instances, telingo- $\lambda$ exhibits faster total runtimes, but as complexity increases, the systems perform competitively. The solving time graph (right) clarifies this discrepancy. Here, the systems compete head-to-head, indicating the runtime difference is primarily driven by an initial grounding overhead in metasp. This penalty is expected, as metasp requires two distinct grounding phases: first to reify the input program, and second to instantiate the meta-encoding. Crucially, because time is not explicitly represented in $\textrm {TEL}$ , the initial reification step does not scale with the horizon. Consequently, this overhead remains relatively flat and becomes negligible on more difficult instances requiring longer horizons.

Next, we evaluate metasp in the context of $\textrm {DEL}$ using the elevator benchmark from (Levesque et al. Reference Levesque, Reiter, Lespérance, Lin and Scherl1997). While we adopt the general experimental setup of Cabalar et al. (Reference Cabalar, Diéguez, Laferriere and Schaub2020), our evaluation employs a more recent version of telingo, which accounts for variations in the reported statistics. This experiment analyzes the impact of $\textrm {DEL}$ -based constraints, designed to eliminate redundant elevator movements, on the number of temporal traces, search choices, and final solver constraints. The full experiment comprises several elevator configurations, serving 5, 7, 9, and 11 floors, each evaluated over five different horizons. To illustrate the different behaviors of the systems, we discuss one representative instance in detail: the 11-floor configuration, which admits two optimal traces of length 17, evaluated at horizon 21. In the baseline configuration without control rules, the instance yields 200900 temporal traces. To compute these, telingo- $\lambda$ and metasp explore search spaces of comparable size (21,6908 vs. 21,4840 choices) and produce a similar number of constraints (3221 vs. 3508). Upon introducing the $\textrm {DEL}$ control rule, the number of traces drops to 2, aligning with the aforementioned optima. While both systems see a massive search space reduction, telingo- $\lambda$ prunes more aggressively (to 50 choices) than metasp (192 choices). However, this optimization incurs a structural cost for both: the constraint count increases from 3221 to 5058 for telingo- $\lambda$ and from 3508 to 6086 for metasp. This behavior, consistent across the benchmark suite, highlights a fundamental key trade-off: both systems achieve a drastic search space reduction at the expense of a significantly inflated grounded representation.

While these findings are promising, a broader empirical and theoretical investigation is necessary to fully characterize this behavior across diverse problem domains. Detailed results for all experiments are available in the metasp repository (Hahn et al. Reference Hahn, Nemes, Romero and Schaub2026).