Higher-Order Timed Automata and Tail Recursion

Bruse, Florian

doi:10.4230/LIPIcs.TIME.2025.5

Higher-Order Timed Automata and Tail Recursion

Florian Bruse

TUM School of Computation, Information and Technology, Technical University of Munich, Munich, Germany

Abstract

Timed Automata (TA) are a popular formalism to model systems in dense linear time. However, due to their finite state-space, they can only model systems with a finitary logical behavior. There are extensions to e.g., timed pushdown systems and timed recursive state machines. Higher-Order Recursion Schemes (HORS) are another popular model for infinite-state, non-regular systems, naturally stratified by their type-theoretic order. We recently introduced Real-Time Recursion schemes as an approximation of HORS to real-time systems.

This paper updates Real-Time Recursion Schemes into Higher-Order Timed Automata, a formalism that defines a tree-shaped timed automaton, which is more suitable to model actual systems. We show that the model-checking problem against the timed version of the modal mu-calculus exhibits the expected complexity bounds, i.e., an increase by one exponential towards the untimed version. We also show that, in the presence of tail recursion, half an exponential can be recovered, mirroring similar gains in the untimed setting. We also give a matching lower bound for the special case of order-1 HORTA. We conjecture that this can be generalized for all orders.

Keywords and phrases:

Timed Automata, Higher-Order Recursion Schemes, Tree Automata, Tail Recursion

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Timed and hybrid models ; Theory of computation

\rightarrow

Tree languages ; Theory of computation

\rightarrow

Automata over infinite objects

DOI:

10.4230/LIPIcs.TIME.2025.5

Event:

32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Editors:

Thierry Vidal and Przemysław Andrzej Wałęga

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Verification of real-time systems plays an ever important role, as more and more aspects of life become computerized. Often, systems are required to not only respond to certain input eventually, but within specific time bounds. For example, electronic stability control or anti-lock braking systems need to respond within fractions of a second.

Timed Automata (TA) [5] are a popular tool to model real-time systems [1, 16]. TA model time not in a discrete fashion, as used in e.g., CTL or the modal $\mu$ -calculus, but rather in a dense linear fashion. The well-known region abstraction allows us to recover finiteness by re-discretization of said dense linear time, which yields decidability (and PSPACE-completeness) of e.g., the model-checking problem for the temporal version of CTL, TCTL [5]. A less well-known real-time logic used in conjunction with timed automata is the timed $\mu$ -calculus ( $T_{\mu}$ ) [17], for which model-checking is EXPTIME-complete.

There are several attempts to generalize the notion of timed automata beyond a finite state space, for example timed recursive state machines [7], recursive timed automata [22], or timed pushdown automata [8, 13]. Recently, we proposed Real-Time Recursion Schemes [3], an extension of the notion of timed automata to Higher-Order Recursion Schemes (HORS). HORS are a well-studied framework in the context of infinite-state verification [14, 18]. A HORS is a higher-order grammar that generates a tree, e.g., the syntax tree of a functional program. The question of HORS model-checking is to decide whether a given alternating parity tree-automaton (APT) accepts the tree generated by the HORS. This is known to be decidable for order- $k$ HORS in $k$ -EXPTIME [20, 19]. We showed in [3] that mixing HORS and real-time systems had the typical effect of increasing the complexity of the model-checking problem by one exponential as compared to the untimed base problem.

This paper extends the idea of Real-Time Recursion Schemes into a proper recursive grammar for timed automata called Higher-Order Timed Automata (HORTA), which makes the problem more natural and rather intuitive to handle. We show that the model-checking problem remains in $(k+1)$ -EXPTIME for the updated problem, which asks whether the timed transition system defined by a HORTA satisfies a given formula of the timed $\mu$ -calculus.

Moreover, we connect the new formalism to existing research in the area of tail recursion. Higher-order model-checking problems like the HORS model-checking problem often have high theoretical complexities, and passing to tail-recursive fragments can shave off half an exponential, not only for recursion schemes [9], but also for model-checking problems where the logic is higher-order [12, 11]. We confirm that these findings also hold for HORTA and the timed $\mu$ -calculus, i.e., that the model-checking problem becomes easier by half an exponential in the tail-recursive setting. We establish a matching lower bound which, for space considerations, is given for the order- $1$ -case only.

The paper is structured as follows: in Sect. 2, we introduce APT, TA, the timed $\mu$ -calculus, HORS, and existing results regarding tail recursion. In Sect. 3 we define HORTA, in Sect. 4 we define the tail-recursive fragment of the HORTA model-checking problem. In Sect. 5, we establish upper bounds for the model-checking problem, and give a matching lower bound for the order- $1$ case in Sect. 6. We conclude in Sect. 7. Most proofs have been omitted due to space considerations.

2 Preliminaries

2.1 Trees and Automata

A tree is a finite, left-closed set $T\subseteq\mathbb{N}^{*}$ , i.e., for all $vi\in T$ , we have $v\in T$ and, moreover, $vi-1\in T$ if $i>0$ . A tree alphabet is a finite, nonempty set $\Sigma$ and a function $\mathit{ar}\colon\Sigma\to\mathbb{N}$ indicating the arity of each symbol. We write $\Sigma_{i}$ for the set of symbols of arity $i$ in $\Sigma$ . A $\Sigma$ -tree is a pair $(T,l)$ of a tree $T$ and a labeling function $l\colon T\mapsto\Sigma$ , such that each $v\in T$ has exactly $\mathit{ar}(l(v))$ successors. We often identify a tree with its labeling function.

Let $S$ be a set. $\mathcal{B}^{+}(S)$ is the set of positive Boolean expressions over $S$ , derived from the grammar $\varphi\coloneqq s\mid\bot\mid\top\mid\varphi\vee\varphi\mid\varphi\wedge\varphi$ with $s\in S$ .

An alternating parity tree-automaton (APT) is a $\mathcal{P}=(Q,\Sigma,\delta,q_{I},\Lambda)$ where $Q$ is a finite, nonempty set of states, $\Sigma$ is a tree alphabet containing a special nullary symbol $\omega$ , $\delta=\bigcup_{i\leq n}\delta^{i}$ is the transition function with $\delta^{i}\colon Q\times\Sigma_{i}\to\mathcal{B}^{+}(Q^{i})$ and $n$ being the maximal arity that occurs in $\Sigma$ . We write $\delta(q,l(v))$ for $\delta^{i}(q,l(v))$ if $\mathit{ar}(l(v))=i$ . Finally, $q_{I}\in Q$ is the starting state and $\Lambda\colon Q\to\mathbb{N}$ is the priority function. The size of an APT is the number of its states.

A run of an APT $\mathcal{P}$ on some $\Sigma$ -tree $T$ (for matching $\Sigma$ ) is a parity game $G(\mathcal{P},T)$ between $\exists$ and $\forall$ , called the acceptance game. It has positions from $T\times(Q\cup\bigcup_{i\leq n}\mathcal{B}^{+}(Q^{i}))$ where $n$ is the maximal arity in $\Sigma$ . Its starting position is $(\epsilon,q_{I})$ . In a position of the form $(v,q)$ , the unique successor is $(v,\delta(q,l(v)))$ . Positions of the forms $(v,\varphi_{1}\vee\varphi_{2})$ and $(v,\varphi_{1}\wedge\varphi_{2})$ have two successors, namely $(v,\varphi_{1})$ and $(v,\varphi_{2})$ . A position of the form $(v,(q_{0},\dotsc,q_{i-1}))$ has $i$ successors $(v0,q_{0}),\dotsc,(v{i-1},q_{i-1})$ , a position of the form $(v,\top)$ or $(v,\bot)$ has no successors. Positions of the forms $(v,\top)$ and $(v,\varphi_{1}\wedge\varphi_{2})$ and $(v,(q_{0},\dotsc,q_{i-1}))$ belong to $\forall$ , all other positions belong to $\exists$ . Finally, the priorities of the game are $\Omega(v,q)=\Lambda(q)$ ; for all other positions we have $\Omega(v,\varphi)=1$ . $\mathcal{P}$ accepts a tree $T$ if $\exists$ wins $G(\mathcal{P},T)$ . In the following, we assume APT to have designated states $q_{\top},q_{\bot}$ from which all, resp. no trees are accepted.

2.2 Higher-Order Recursion Schemes

Instead of the classical definition of Higher-Order Recursion Schemes (HORS, cf. e.g., [18]), we use a version going back to Damm [14] and re-introduced by Walukiewicz and Salvati [21], using the $\lambda Y$ -calculus as syntax.

Types and Terms.

The set of types is defined inductively via $\tau\Coloneqq\bullet\mid\tau\to\tau$ where $\bullet$ is the type of trees, $\bullet\to\bullet$ is the type of functions that consume a tree and yield a tree, etc. We write $\tau^{i}\to\bullet$ for the type $\tau\to\dotsb\tau\to\bullet$ with $i$ many copies of $\tau$ . The order of a type is defined via $\mathit{ord}(\bullet)=0$ and $\mathit{ord}(\tau_{1}\to\tau_{2})=\max\{1+\mathit{ord}(\tau_{1}),\mathit{ord}(% \tau_{2})\}$ .

Let $\Sigma$ be a tree alphabet. Each $a\in\Sigma$ of arity $i$ is a tree constructor of type $\bullet^{i}\to\bullet$ . Let $\mathcal{L}$ be a set of typed $\lambda$ variables, $\mathcal{F}$ be a set of typed Y variables. Lower case letters $a,b,\dotsc$ denote tree constructors, lower case letters $x,y,\dotsc$ denote $\lambda$ variables, upper case letters $F,G,\dotsc$ denote Y variables. If necessary, $(x\colon\tau)$ , $(F\colon\tau)$ indicates the type of a variable.

Given $\Sigma,\mathcal{L},\mathcal{F}$ , the set of $\lambda Y$ terms is defined inductively: a tree constructor of type $\bullet^{i}\to\bullet$ is a term of type $\bullet^{i}\to\bullet$ , a lambda variable $x\colon\tau$ and a Y variable $F\colon\tau$ are terms of type $\tau$ . Given $x\colon\tau_{1}$ and a term $t$ of type $\tau_{2}$ , $\lambda(x\colon\tau).\ t$ is a term of type $\tau_{1}\to\tau_{2}$ . Given terms $t_{1},t_{2}$ of type $\tau_{2}\to\tau_{1}$ and $\tau_{2}$ , resp., $(t_{1}\ t_{2})$ is a term of type $\tau_{1}$ . If $F\colon\tau$ is a Y variable and $t$ is a term of type $\tau$ , then $Y(F\colon\tau).\ t$ is a term of type $\tau$ .

$t[t^{\prime}/x]$ denotes capture-avoiding substitution of $t^{\prime}$ for all free occurrences of $x$ in $t$ , and similarly for $t[t^{\prime}/F]$ , assuming that the types match. Each variable may also be bound at most once in a term. Hence, for closed terms there is a function $\mathit{term}$ that maps each $Y$ variable $F$ to $\mathit{term}(F)$ , defined as $t$ if the unique binding of $F$ is $YF.\ t$ . The order of a term is that of the highest order of any of its subterms, its size the number of its distinct subterms.

Semantics.

Besides $\alpha$ -conversion, i.e., variable renaming, the $\lambda Y$ calculus has $\beta$ -reduction and $\delta$ -reduction. $\beta$ -reduction $\to_{\beta}$ reduces $((\lambda x.\ t)\ t^{\prime})$ , where $x$ and $t^{\prime}$ have the same type, to $t[t^{\prime}/x]$ . $\delta$ -reduction $\to_{\delta}$ reduces $YF.\ t$ to $t$ and $F$ to $\mathit{term}(F)$ . The reflexive transitive closure of $\to_{\beta}\cup\to_{\delta}$ is $\to^{*}_{\beta\delta}$ . Since both $\beta$ -reduction and $\delta$ -reduction maintain the type of a term, so does $\to^{*}_{\beta\delta}$ , and this relation is confluent. A closed term of type $\bullet$ is in weak head normal form if it is of the form $a\ t_{0}\dotsb t_{j}$ . Not every $\lambda Y$ term reduces to a head normal form.

Let $\Sigma$ be a tree signature and let $\omega$ be a new nullary symbol, i.e, of type $\bullet$ . We define the Böhm tree $\mathit{BT}(t)$ of a closed term of type $\bullet$ as follows: If $t$ does not reduce via $\to^{*}_{\beta\delta}$ to a weak head normal form, then $\mathit{BT}(t)=\omega$ , i.e., the tree has just one node. Otherwise, let $a\ t_{0}\dotsb t_{j}$ be a weak head normal form of $t$ . The root of $\mathit{BT}(t)$ is labeled by $a$ , and its successors are, in order, the roots of $\mathit{BT}(t_{0}),\dotsc,\mathit{BT}(t_{j})$ . Due to confluence, this definition is sound.

The HORS model-checking problem (defined via $\lambda Y$ terms) is the following: Given a closed term $t$ of type $\bullet$ over $\Sigma$ and an APT $\mathcal{A}$ with alphabet $\Sigma\cup\{\omega\colon\bullet\}$ , does $\mathcal{A}$ accept $\mathit{BT}(t)$ ? For terms of order $k\geq 0$ , this is known to be a $k$ -EXPTIME complete problem [20].

2.3 Timed Automata

Let $\mathcal{X}=\{\texttt{x},\texttt{y},\dotsc\}$ be a set of $\mathbb{R}^{\geq 0}$ -valued variables, called clocks. $\mathit{CC}(\mathcal{X})$ is the set of clock constraints over $\mathcal{X}$ , defined as conjunctive formulas over $\top$ and $\texttt{x}\oplus c$ for $\texttt{x}\in\mathcal{X}$ and $c\in\mathbb{N}$ , where $\oplus\in\{\leq,<,>,\geq\}$ . Clock constraints are denoted by $\chi,\chi^{\prime}$ etc.

A clock evaluation is a mapping $\eta\colon\mathcal{X}\to\mathbb{R}^{\geq 0}$ ; it satisfies a clock constraint as follows: (i) $\eta\models\top$ always, (ii) $\eta\models\texttt{x}\oplus c$ iff $\eta(\texttt{x})\oplus c$ and (iii) $\eta\models\varphi_{1}\wedge\varphi_{2}$ iff $\eta\models\varphi_{1}$ and $\eta\models\varphi_{2}$ . For a clock evaluation $\eta$ and $d\in\mathbb{R}^{\geq 0}$ , we write $\eta{+}d$ for the clock evaluation defined via $(\eta{+}d)(\texttt{x})=\eta(\texttt{x})+d$ for all $\texttt{x}\in\mathcal{X}$ . For $R\subseteq\mathcal{X}$ , $\eta|_{R}$ is the clock evaluation defined via $\eta|_{R}(\texttt{x})=\eta(\texttt{x})$ if $x\notin R$ and $\eta|_{R}(\texttt{x})=0$ if $\texttt{x}\in R$ .

Let $\mathit{Prop}$ be a finite set of propositions. A timed automaton over clocks in $\mathcal{X}$ and with propositions in $\mathit{Prop}$ is an $\mathcal{A}=(L,\mathcal{X},\ell_{0},\iota,\Delta,\lambda)$ where (i) $L$ is the set of locations of the timed automaton, including the initial location $\ell_{0}$ , (ii) $\mathcal{X}$ is a finite set of clocks, (iii) $\iota\colon L\to\mathit{CC}(\mathcal{X})$ assigns a clock constraint called an invariant to each location, (iv) $\Delta\subseteq L\times\mathit{CC}(\mathcal{X})\times 2^{\mathcal{X}}\times L$ is a finite set of transitions; we write $\ell\mathop{{\hbox{{$\mathrel{\mathop{\hbox to20.67091pt{\rightarrowfill}}% \limits^{g,R}}$}}}}\ell^{\prime}$ for $(\ell,g,R,\ell^{\prime})\in\delta$ . In such a transition, $g$ is the guard and $R$ are the resets of the transition. Finally, (v) $\lambda\colon L\to 2^{\mathit{Prop}}$ labels each location with the propositions valid there. The index $m(\mathcal{A})$ of a timed automaton $\mathcal{A}$ is the largest constant that occurs in its guards or invariants. Its size is defined as

|\mathcal{A}|=|\Delta|\cdot(2\cdot\log(|L|)+|\mathcal{X}|^{2}\cdot\log m(% \mathcal{A}))+|L|\cdot(\log|\mathcal{X}|^{2}\cdot\log m(\mathcal{A}))+|L|\cdot% |\mathit{Prop}|.

due to the coding of the constants in clock constraints in binary. A TA defines a timed Transition System (tTS), to be defined in more general fashion in Sect. 3.

2.4 The Timed $\mu$ -Calculus

We define the timed modal $\mu$ -calculus ( $T_{\mu}$ ) following [17]. Let $\mathcal{X}$ be a set of clocks and let $\mathcal{Y}$ disjoint from $\mathcal{X}$ be a set of specification clocks. Let $\mathit{Prop}$ be a set of propositions and let $\mathcal{V}$ be a set of fixpoint variables. A formula of $T_{\mu}$ is one derived from the following grammar:

\varphi\Coloneqq p\mid X\mid\chi\mid\neg\varphi\mid\varphi\vee\varphi\mid% \varphi\wedge\varphi\mid\varphi\rhd\varphi\mid\varphi\boxminus\varphi\mid% \texttt{z}.\ \varphi\mid\mu X.\ \varphi\mid\nu X.\ \varphi

where $p\in\mathit{Prop},X\in\mathcal{V},\chi\in\mathit{CC}(\mathcal{X}\cup\mathcal{Y})$ and $\texttt{z}\in\mathcal{Y}$ . Moreover, every variable $X$ must be bound exactly once and occur under an even number of negations in $\mu X.\ \varphi$ or $\nu X.\ \varphi$ , a standard convention for the modal $\mu$ -calculus. This induces, for each $T_{\mu}$ formula $\varphi$ , a function $\mathit{fp}$ where $\mathit{fp}(X)$ is the unique $\psi$ with $\mu X.\ \psi$ or $\nu X.\ \psi$ a subformula of $\varphi$ . Moreover, we assume w.l.o.g. that every $T_{\mu}$ formula is guarded in the sense that, on the path from $\mu X.\ \psi$ or $\nu X.\ \psi$ to $X$ in the syntax tree of the formula, there is an instance of $\rhd$ or $\boxminus$ . Analogously to the ordinary $\mu$ -calculus [10], every $T_{\mu}$ formula can be converted into an equivalent guarded one, potentially at the cost of exponential blowup¹¹1This blowup can be avoided at the cost of extra complexity, so we decide to simply stipulate guardedness for the sake of simplicity..

$\texttt{z}.\ \varphi$ resets the specification clock z to $0$ . Hence, patterns like $\texttt{z}.\ \dots\texttt{z}=4\dots$ serve to test for elapsed time. The intuition for $\varphi_{1}\rhd\varphi_{2}$ is that of a temporal next operator: it is satisfied if $\varphi_{2}$ is true after a sequence of a delay, a discrete transition, and another delay, and $\varphi_{1}$ is true all the way before. The operator $\boxminus$ is the dual of it, i.e., a temporal next with universal quantification over delays and transitions.

Let $\mathcal{T}=(\mathcal{S},\mathop{{\hbox{{$\mathrel{\mathop{\hbox to8.19447pt{% \rightarrowfill}}\limits}$}}}},s_{0},\lambda)$ be a tTS, let $\alpha\colon\mathcal{V}\to 2^{\mathcal{S}}$ be a variable assignment. The semantics $\llbracket\varphi\rrbracket_{\mathcal{T}}^{\alpha}$ of a $T_{\mu}$ formula $\varphi$ is defined inductively via

$\displaystyle\llbracket p\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\{s\in\mathcal{S}\mid p\in\lambda(s)\}$	$\displaystyle\llbracket X\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\alpha(X)$
$\displaystyle\llbracket\chi\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\{s\in\mathcal{S}\mid s\models\chi\}$	$\displaystyle\llbracket\texttt{z}.\ \psi\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\{s\in\mathcal{S}\mid s\|_{\{\texttt{z}\}}\in\llbracket\psi% \rrbracket_{\mathcal{T}}^{\alpha}\}$
$\displaystyle\llbracket\psi_{1}\vee\psi_{2}\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\llbracket\psi_{1}\rrbracket_{\mathcal{T}}^{\alpha}\cup% \llbracket\psi_{2}\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle\llbracket\psi_{1}\wedge\psi_{2}\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\llbracket\psi_{1}\rrbracket_{\mathcal{T}}^{\alpha}\cap% \llbracket\psi_{2}\rrbracket_{\mathcal{T}}^{\alpha}$
$\displaystyle\llbracket\neg\psi\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\mathcal{S}\setminus\llbracket\psi\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle\llbracket\psi_{1}\boxminus\psi_{2}\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\llbracket\neg(\neg\psi_{1}\boxminus\neg\psi_{2})\rrbracket_{% \mathcal{T}}^{\alpha}$

with

	$\displaystyle\llbracket\mu X.\ \psi\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\bigcap\{\mathcal{S}^{\prime}\subseteq\mathcal{S}\mid\llbracket% \psi\rrbracket_{\mathcal{T}}^{\alpha[X\mapsto\mathcal{S}^{\prime}]}\subseteq% \mathcal{S}^{\prime}\}$
	$\displaystyle\llbracket\nu X.\ \psi\rrbracket_{\mathcal{T}}^{\alpha}$	$\displaystyle=\bigcup\{\mathcal{S}^{\prime}\subseteq\mathcal{S}\mid\llbracket% \psi\rrbracket_{\mathcal{T}}^{\alpha[X\mapsto\mathcal{S}^{\prime}]}\supseteq% \mathcal{S}^{\prime}\}$

and where $\llbracket\psi_{1}\rhd\psi_{2}\rrbracket_{\mathcal{T}}^{\alpha}$ is defined as

\{s\mid\text{ ex.\ }s^{\prime}\in\mathcal{S},d,d^{\prime}\in\mathbb{R}^{\geq 0% }\text{ s.t.\ }s+d\mathop{{\hbox{{$\mathrel{\mathop{\hbox to8.19447pt{% \rightarrowfill}}\limits}$}}}}s^{\prime}\text{ and }s^{\prime}+d^{\prime}\in% \llbracket\psi_{2}\rrbracket_{\mathcal{T}}^{\alpha},\\ \text{ and }s+d^{\prime\prime}\in\llbracket\psi_{1}\rrbracket_{\mathcal{T}}^{% \alpha}\text{ f.a.\ }0\leq d^{\prime\prime}\leq d\text{ and }s^{\prime}+d^{% \prime\prime\prime}\in\llbracket\psi_{1}\vee\psi_{2}\rrbracket_{\mathcal{T}}^{% \alpha}\text{ f.a.\ }0\leq d^{\prime\prime\prime}\leq d^{\prime}\}.

Here, the temporal next relation $\rhd$ is defined as the composition of a delay, a discrete transition, and another delay. The clause that all states after the discrete transition need to satisfy $\psi_{1}\vee\psi_{2}$ is standard to cope with the fact that there might not be a smallest delay that makes $\psi_{2}$ true. Standard patterns in temporal logic, e.g., $\mathop{\mathtt{E}}(p\mathbin{\mathtt{U}}_{[3,4]}q)$ , which says that there is a path on which $p$ holds until $q$ holds, and that $q$ holds after time elapsed between $3$ and $4$ time units, can be expressed as e.g., $\texttt{z}.\ \mu X.\ (q\wedge 3\leq\texttt{z}\wedge\texttt{z}\leq 4)\vee p\rhd X$ .

The model-checking problem for $T_{\mu}$ is then to decide, given a timed automaton and a $T_{\mu}$ formula $\varphi$ , whether $\mathcal{T}\models\varphi$ where $\mathcal{T}$ is the tTS defined by the timed automaton.

Proposition 1 ([2]).

The model-checking problem for $T_{\mu}$ is EXPTIME-complete.

2.5 Tail Recursion

Bounded-Alternation Parity Automata.

Let $\Sigma$ be partitioned into $\Sigma_{\mathsf{re}}\cup\Sigma_{\mathsf{ur}}$ . Let $\mathcal{P}=(Q,\Sigma,\delta,q_{I},\Lambda)$ be an APT such that $Q$ is partitioned into sets $\{q_{\top},q_{\bot}\}\cup Q_{\mathsf{ur}},Q_{1},\dotsc,Q_{m}$ for some $m$ . Let $q\in Q_{j}$ for some $1\leq j\leq m$ and let $a\in\Sigma^{2}$ . We say that $\mathcal{A}$ is branching at $q$ and $a$ if $\delta(q,a)=(q_{1},q_{\top})\vee(q_{\top},q_{2})$ with $q_{1},q_{2}\in Q_{j}\cup\{q_{\top},q_{\bot}\}$ or $\delta(q,a)=(q_{1},q_{2})$ with $q_{2}\in Q_{j}\cup\{q_{\top},q_{\bot}\}$ and $q_{1}\in Q_{j-1}\cup\dotsb\cup Q_{1}\cup\{q_{\top},q_{\bot}\}$ . It is universal at $q$ and $a$ if $\delta(q,a)=(q_{1},q_{2})$ with both $q_{1},q_{2}\in Q_{j}\cup\{q_{\top},q_{\bot}\}$ , or $\delta(q,a)=(q_{1},q_{\top})\vee(q_{\top},q_{2})$ with $q_{1}\in Q_{j-1}\cup\dotsb\cup Q_{1}\cup\{q_{\top},q_{\bot}\}$ and $q_{2}\in Q_{j}\cup\{q_{\top},q_{\bot}\}$ .

$\mathcal{P}$ is called a bounded-alternation APT (baAPT) if it satisfies the following conditions:

1.

$Q$ is partitioned into sets $\{q_{\top},q_{\bot}\},Q_{\mathsf{ur}},Q_{1},\dotsc,Q_{m}$ as per above.
2.

For each $1\leq i\leq m$ , each $Q_{i}$ is labeled as either branching or universal. $Q_{\mathsf{ur}}$ is not labeled.
3.

If $Q_{i}$ is branching, then for each $q\in Q_{i}$ and for each $a\in\Sigma_{\mathsf{re}}$ , $\mathcal{A}$ is branching at $q$ and $a$ . If $Q_{i}$ is universal, then for each $q\in Q_{i}$ and for each $a\in\Sigma_{\mathsf{re}}$ , $\mathcal{A}$ is universal at $q$ and $a$ .
4.

For each $q\in Q$ and $a\in\Sigma^{i}_{\mathsf{ur}}$ , we have that $\delta(q,a)\in\mathcal{B}^{+}(Q^{i}_{\mathsf{ur}})$ .
5.

For each $q\in Q_{\mathsf{ur}}$ and $a\in\Sigma^{i}_{\mathsf{re}}$ , we have that $\delta(q,a)\in\mathcal{B}^{+}((Q\setminus Q_{\mathsf{ur}})^{i})$ .

The intuition here is as follows: The acceptance problem of a baAPT in which each state is branching or in which each state is universal can be reduced to a one-player game. The acceptance problem for such a baAPT with empty set $Q_{\mathsf{ur}}$ is a bounded-alternation game. For general baAPT, the reduction to a bounded-alternation game is still possible if offending states are in a set of lower index and there is an a priori bound on the number of times a play passes through states in $Q_{\mathsf{ur}}$ . The definition of tail-recursive HORS below yields this bound.

Tail-Recursion for $\lambda Y$ Terms.

Let $t$ be a term of the $\lambda Y$ calculus over $\Sigma_{\mathsf{re}}\cup\Sigma_{\mathsf{ur}}$ , $\mathcal{L}$ and $\mathcal{F}$ . It is called tail-recursive if it satisfies the following conditions:

1.

For all subterms of $t$ of the form $t_{1}\ t_{2}$ , the operand-side subterm $t_{2}$ has no free $\mathcal{F}$ variables.
2.

For all subterms of the form $a\ t_{0}\dotsb t_{j}$ with $a\in\Sigma_{\mathsf{ur}}$ , none of the $t_{i}$ has free $\mathcal{F}$ variables.

Note that there are no restrictions w.r.t. variables in $\mathcal{L}$ .

Definition 2.

Let $\Sigma$ be partitioned into $\Sigma_{\mathsf{re}}\cup\Sigma_{\mathsf{ur}}$ . Let $t$ be a closed tail-recursive term of type $\bullet$ in the $\lambda Y$ calculus over $\Sigma$ , and let $\mathcal{P}$ be a baAPT. The problem of tail-recursive HORS model checking is to decide whether $\mathcal{P}$ accepts $\mathit{BT}(t)$ .

Proposition 3 ([9]).

The problem of tail-recursive HORS model checking (i.e., against a baAPT) for terms of order $k>0$ is complete for $(k{-}1)$ -EXPSPACE.

3 Higher-Order Recursive Timed Automata

Timed automata define tTS, where each state is a pair of a location and a clock evaluation, the former which defines the propositonal labeling of the state. Transitions in tTS are either delay transitions that let time flow but keep the location component, or discrete transitions that keep time fixed, change the location, and reset clocks as indicated by the transition. The first kind of transition respects location invariants, while the second kind respects guards.

The idea for recursively defined tTS is that locations are not a fixed, finite set, but are the nodes of a tree generated by a $\lambda Y$ term. The propositional labeling is derived from the labeling of the respective node, i.e., the tree constructor in question. Moreover, we define HORS for tTS in such a way that a tree constructor also carries information on the location invariant associated to it, and the guards and resets of its successors.

Definition 4.

Let $\mathcal{X}$ be a finite set of clocks and let $\mathit{Prop}$ be a finite set of propositions. A timed tree alphabet (over $\mathcal{X}$ and $\mathit{Prop}$ ) is a finite, nonempty set $\Sigma$ together with functions $\mathit{ar},\lambda,\iota,\mathit{trns}$ of domain $\Sigma$ where, for each $a\in\Sigma$ ,

1.

$\mathit{ar}(a)\in\mathbb{N}$ indicates the arity of the symbol (as for standard tree alphabets),
2.

$\lambda(a)\subseteq{\mathit{Prop}}$ indicates the propositional labeling of a node labeled by the symbol,
3.

$\iota(a)\in\mathit{CC}(\mathcal{X})$ indicates the invariant of a node labeled by the symbol, and
4.

$\mathit{trns}(a)\in(\mathit{CC}(\mathcal{X})\times 2^{\mathcal{X}})^{i}$ where $i=\mathit{ar}(a)$ indicates the guards and resets on the edges to the $i$ many successors of a node labeled by the symbol.

We write $\mathit{trns}_{i}(a)$ to denote the $i$ th element of the tuple $\mathit{trns}(a)$ .

Of course, a timed tree alphabet is a tree alphabet by ignoring the extra functions. A tree labeled by such a timed alphabet gives rise to a tTS as follows.

Definition 5.

Let $\Sigma$ be a timed tree alphabet over $\mathcal{X}$ and $\mathit{Prop}$ and let $(T,l)$ be a $\Sigma$ -tree. The tTS defined by $(T,l)$ is $\mathcal{T}_{T}=(\mathcal{S},\mathop{{\hbox{{$\mathrel{\mathop{\hbox to8.19447% pt{\rightarrowfill}}\limits}$}}}},s_{0},\lambda)$ where

$\blacksquare$

$\mathcal{S}=\{(v,\eta)\mid\eta\models\iota(l(v))\}$ , where $v\in T$ and $\eta\colon\mathcal{X}\to\mathbb{R}^{\geq 0}$ ,
$\blacksquare$

the initial state is $(\epsilon,\eta_{0})$ with $\eta_{0}(\texttt{x})=0$ f.a. $\texttt{x}\in\mathcal{X}$ ,
$\blacksquare$

delay transitions keep the tree node but let time flow: for any $(v,\eta)\in\mathcal{S}$ and $d\in\mathbb{R}^{\geq 0}$ we have a transition $(v,\eta)\mathop{{\hbox{{$\mathrel{\mathop{\hbox to12.35735pt{\rightarrowfill}}% \limits^{d}}$}}}}(v,\eta+d)$ if $\eta+d^{\prime}\models\iota(l(v))$ for all $0\leq d^{\prime}\leq d$ .
$\blacksquare$

discrete transitions are derived from $\mathit{trns}(l(v))$ : for all $(v,\eta)\in\mathcal{S},i<\mathit{ar}(l{v})$ , we have $(v,\eta)\mathop{{\hbox{{$\mathrel{\mathop{\hbox to8.19447pt{\rightarrowfill}}% \limits}$}}}}(vi,\eta|_{R})$ if $\mathit{trns}_{i}(l(v))=(\chi,R)$ and $\eta\models\chi$ and $\eta|_{R}\models\iota(l(vi))$ ,
$\blacksquare$

the propositional labeling $\lambda$ feeds through the labeling of a tree node, i.e., $\lambda(v,\eta)=\lambda(l(v))$ ,
$\blacksquare$

all states are labeled by the clock constraints that hold there, i.e., $(v,\eta)\models\chi$ iff $\eta\models\chi$ .

Note that $\mathcal{T}_{T}$ is generally not a tree due to additivity of time: there are uncountably many paths from $(v,\eta)$ to $(v,\eta+d)$ for any $d>0$ s.t. the location invariant is satisfied. Other than this, the transition system is a tree though.

A $\lambda Y$ term $t$ over a timed alphabet is called a Higher-Order Recursive Timed Automaton (HORTA). It generates a tTS $\mathcal{T}_{t}$ via the tree generated from the term. Its order is that of the order of the underlying $\lambda Y$ term. The index $m(t)$ of a HORTA is the largest constant that occurs in its guards or invariants, its arity $\mathit{ar}(t)$ is the maximal arity of a symbol in its tre alphabet. The size of a HORTA is $|\!|t|\!|=|t|\cdot|\Sigma|\cdot(|\mathit{Prop}|+|\mathcal{X}|^{2}\cdot m(% \mathcal{A})\cdot\mathit{ar}(t))$ where $|t|$ defines the size of the underlying $\lambda Y$ term.

The HORTA model-checking problem is then the following:

given:	a HORTA $t$ and a formula $\varphi$ of the timed $\mu$ -calculus
decide:	does $\mathcal{T}_{{t}}\models\varphi$ hold?

An example can be found in the appendix.

4 Tail Recursion

Let $\mathcal{X}$ be a set of clocks, $\mathcal{Y}$ be a set of specification clocks and $\mathit{Prop}$ be a set of atomic propositions with $p_{\text{sf}}\in\mathit{Prop}$ a designated proposition. This proposition takes the role of a tree constructor from $\Sigma_{\mathsf{ur}}$ for tail-recursive terms, i.e., it signals tree nodes s.t. its subtrees are defined using terms without free $Y$ variables. Hence, given a HORTA, this designated proposition $p_{\text{sf}}$ partitions its tree alphabet $\Sigma$ into $\Sigma_{\mathsf{ur}}=\{a\mid p_{\text{sf}}\in\lambda(a)\}$ and $\Sigma_{\mathsf{re}}=\{a\mid p_{\text{sf}}\notin\lambda(a)\}$ . A HORTA is tail recursive if it is tail recursive as a HORS using this partition.

Now let $\mathcal{V}=\mathcal{V}^{\mathsf{br}}_{1}\cup\mathcal{V}^{\mathsf{un}}_{1}\cup% \dotsb\cup\mathcal{V}^{\mathsf{br}}_{m}\cup\mathcal{V}^{\mathsf{un}}_{m}\cup% \mathcal{V}_{\mathsf{ur}}$ be the set of fixpoint variables, partitioned into $2m+1$ different sets. Each such variable plays the same role as a state in a baAPT, including being either branching, universal, or unrestricted, an being partitioned into different sets. Hence, the the annotations mark the variables as branching, universal, or unrestricted (superscript), and fix the respective set of the partition (subscript).

A $T_{\mu}$ formula has bounded-alternation if it can be derived from $\psi_{m}^{\mathsf{br}}$ or $\psi_{m}^{\mathsf{un}}$ in the following grammar:

	$\displaystyle\psi^{\mathsf{sf}}$	$\displaystyle=\texttt{t\!t}\mid\texttt{f\!f}\mid p\mid\neg p\mid\chi\mid\neg% \chi\mid\psi^{\mathsf{sf}}\vee\psi^{\mathsf{sf}}\mid\psi^{\mathsf{sf}}\wedge% \psi^{\mathsf{sf}}\mid p_{\text{sf}}\wedge\psi^{\mathsf{ur}}$
	$\displaystyle\psi^{\mathsf{br}}_{m}$	$\displaystyle=\psi^{\mathsf{sf}}\mid X_{m}^{\mathsf{br}}\mid\neg\psi_{m-1}\mid% \psi^{\mathsf{br}}_{m}\vee\psi^{\mathsf{br}}_{m}\mid\psi_{m-1}\wedge\psi^{% \mathsf{br}}_{m}\mid\psi_{m-1}\rhd\psi_{m}^{\mathsf{br}}\mid\mu X_{m}^{\mathsf% {br}}.\ \psi_{m}^{\mathsf{br}}\mid\nu X_{m}^{\mathsf{br}}.\ \psi_{m}^{\mathsf{% br}}$
	$\displaystyle\psi^{\mathsf{un}}_{m}$	$\displaystyle=\psi^{\mathsf{sf}}\mid X_{m}^{\mathsf{un}}\mid\neg\psi_{m-1}\mid% \psi_{m-1}\vee\psi^{\mathsf{un}}_{m}\mid\psi^{\mathsf{un}}_{m}\wedge\psi^{% \mathsf{un}}_{m}\mid\psi_{m-1}\boxminus\psi_{m}^{\mathsf{un}}\mid\mu X_{m}^{% \mathsf{un}}.\ \psi_{m}^{\mathsf{un}}\mid\nu X_{m}^{\mathsf{un}}.\ \psi_{m}^{% \mathsf{un}}$
	$\displaystyle\vdots\quad$	$\displaystyle\qquad\vdots$
	$\displaystyle\psi^{\mathsf{br}}_{1}$	$\displaystyle=\psi^{\mathsf{sf}}\mid X_{1}^{\mathsf{br}}\mid\psi^{\mathsf{br}}% _{1}\vee\psi^{\mathsf{br}}_{1}\mid\psi^{\mathsf{sf}}\wedge\psi^{\mathsf{br}}_{% 1}\mid\psi^{\mathsf{sf}}\rhd\psi_{1m}^{\mathsf{br}}\mid\mu X_{m}^{\mathsf{br}}% .\ \psi_{m}^{\mathsf{br}}\mid\nu X_{m}^{\mathsf{br}}.\ \psi_{m}^{\mathsf{br}}x$
	$\displaystyle\psi^{\mathsf{un}}_{1}$	$\displaystyle=\psi^{\mathsf{sf}}\mid X_{1}^{\mathsf{un}}\mid\psi^{\mathsf{sf}}% \vee\psi^{\mathsf{un}}_{1}\mid\psi^{\mathsf{un}}_{1}\wedge\psi^{\mathsf{un}}_{% 1}\mid\psi^{\mathsf{sf}}\boxminus\psi_{1}^{\mathsf{un}}\mid\mu X_{1}^{\mathsf{% un}}.\ \psi_{1}^{\mathsf{br}}\mid\nu X_{1}^{\mathsf{un}}.\ \psi_{1}^{\mathsf{% br}}$
	$\displaystyle\psi^{\mathsf{ur}}$	$\displaystyle=\psi^{\mathsf{sf}}\mid\psi^{\mathsf{ur}}\vee\psi^{\mathsf{ur}}% \mid\psi^{\mathsf{ur}}\wedge\psi^{\mathsf{ur}}\mid\psi^{\mathsf{sf}}\rhd\psi^{% \mathsf{sf}}\mid\psi^{\mathsf{sf}}\boxminus\psi^{\mathsf{sf}}$
		$\displaystyle\quad\mid\mu X^{\mathsf{ur}}.\ \psi^{\mathsf{ur}}\mid\nu X^{% \mathsf{ur}}.\ \psi^{\mathsf{ur}}\mid(\neg p_{\text{sf}}\wedge\psi_{m})$

where $X^{\mathsf{br}}_{i},X^{\mathsf{un}}_{i}$ are in the respective sets of variables for all $i$ , and so is $X^{\mathsf{ur}}$ . A term $\psi_{i}$ can denote both $\psi_{i}^{\mathsf{un}}$ and $\psi_{i}^{\mathsf{br}}$ .

We give some intuition for this definition of bounded-alternation $T_{\mu}$ -formulas. A key point for tail-recursive behavior is limited boolean alternation, i.e. between $\vee$ and $\wedge$ . The reason for that is that space-bounded algorithms need bounded boolean alternation, for (fully) alternating space is exponential time. baAPT achieve this by (partially) limiting the acceptance game to a game that is played by one player only, either $\exists$ or $\forall$ , with the other player only making token moves without associated freedom of decision. This is then captured in the intuition for bounded-alternation $T_{\mu}$ formulas in a syntactic way.

However, a better intuition is that a formula is alternation-free if it either does not contain $\wedge$ and $\boxminus$ , or if it does not contain $\vee$ and $\rhd$ , and no negations. An example of this is $\mu X.\ p\vee(\texttt{t\!t}\rhd X)$ , or $\mu X.\ p\wedge(\texttt{t\!t}\boxminus X)$ . Note that the polarity of the fixpoint does not matter here.

Limited alternation is then allowed by stratifying these formulas (via the indices in e.g., $\psi^{\mathsf{br}}_{m},\dotsc,\psi^{\mathsf{br}}_{1}$ ) and allowing one-time use of forbidden operators at the price of dropping to a lower level in the hierarchy. Of course, formulas that contain no recursive definitions at all, e.g., those in $\psi^{\mathsf{sf}}$ are also safe. Hence, we obtain e.g.,

\mu X.(\texttt{t\!t}\rhd x)\vee\big(\neg p\wedge(q\vee\nu Z.\ p\wedge(\texttt{% t\!t}\boxminus Z))\big).

Since bounded-alternation formulas are to be evaluated over tTS defined by tail-recursive $\lambda Y$ terms, there is an additional ingredient: In tail-recursive $\lambda Y$ terms, subterms in operand position cannot contain free $Y$ variables, whence the tree generated by such a subterm is completely independent of the rest of the term (excluding arguments of its own, of course). Moreover, we use special alphabet symbols (those in $\Sigma^{\mathsf{ur}}$ ) to signal that a term appears e.g., in operand position, or that it contains no free $Y$ variables. Since the tree defined by such a term is independent of the rest of the tree, and since this can only repeat a polynomial amount of times (due to passing to a strict subterm), a model-checking procedure can solve the problem for the tree generated by the subterm first, and then return to the model-checking problem for the overall tree. Since this is such an independent subproblem, it is not harmful to “reset” the amount of boolean alternation possible in a $T_{\mu}$ formula/a baAPT. This is what happens in formulas of the form $\psi^{\mathsf{ur}}$ , which have nontrivial semantics only in states where $p_{\text{sf}}$ is true (and, hence a tree constructor from $\Sigma^{\mathsf{ur}}$ was read, whence we are in such an independent subproblem). Note that it is not important that this generates a polynomial bound on the number of “alternation resets” in a run of a baAPT/the evaluation of a bounded-alternation $T_{\mu}$ formula. In general, there is no such bound. However, the model-checking problem will always only generate a polynomial stack of open subproblems due to alternation resets, and that suffices to yield the complexity bound.

The example in the appendix contains a simple example of a pair of a tail-recursive HORTA and a bounded-alternation $T_{\mu}$ formula.

5 Upper Bounds for Model-Checking

The goal of this section is to establish upper bounds for model checking of the trees generated by HORTA (tail recursive or not) against $T_{\mu}$ formulas. For the rest of the section, fix a tree alphabet $\Sigma$ , a $\lambda Y$ term $t$ and a $T_{\mu}$ formula $\varphi$ . Assume w.l.o.g. that $\varphi$ is in negation normal form, i.e., that negations appear only in front of propositions or clock constraints.

5.1 The Region Abstraction

The region abstraction is a classical result (see e.g., [4] or [6], Def. 9.42), that maps the infinite transition system defined by a TA onto a finite transition system. While we work with tTS defined by HORTA, the key point is the same: the region abstraction uses an equivalence relation $\simeq_{m}$ , for $m\in\mathbb{N}$ , on clock evaluations. Let $\mathcal{X}$ be a set of clocks, specification or otherwise. Then $\simeq_{m}$ is defined as follows: $\eta\simeq_{m}\eta^{\prime}$ iff

	$\displaystyle\text{for all }\texttt{x}\in\mathcal{X}:$	$\displaystyle\eta(\texttt{x})>m\text{ and }\eta^{\prime}(\texttt{x})>m$
		$\displaystyle\text{or }\lfloor\eta(\texttt{x})\rfloor=\lfloor\eta^{\prime}(% \texttt{x})\rfloor\text{ and }\mathit{frac}(\eta(\texttt{x}))=0\Leftrightarrow% \mathit{frac}(\eta^{\prime}(\texttt{x}))=0$
		$\displaystyle\quad\quad\text{and for all }\texttt{y}\in\mathcal{X}\text{ with % }\eta(\texttt{y})\leq m\text{ and }\eta^{\prime}(\texttt{y})\leq m:$
		$\displaystyle\qquad\qquad\mathit{frac}(\eta(\texttt{x}))\leq\mathit{frac}(\eta% (\texttt{y}))\Leftrightarrow\mathit{frac}(\eta^{\prime}(\texttt{x}))\leq% \mathit{frac}(\eta^{\prime}(\texttt{y})).$

$\mathit{frac}(r)$ is the fractional part of a real number. Clock evaluations are equivalent if, for each clock, (i) either both clocks have a value greater than $m$ , or (ii) they compare in the same way with respect to all integers $\leq m$ . Moreover, the passage of time makes equivalent evaluations reach the next integral value first for the same clock. $\simeq_{m}$ is an equivalence relation for any $m$ ; an equivalence class in $\simeq_{m}$ is called a region. The equivalence class of $\eta$ under $\simeq_{m}$ is $[\eta]_{m}$ (or just $[\eta]$ when $m$ is clear). We define the notion of a successor region:

Definition 6.

Let $\simeq_{m}$ denote the region equivalence w.r.t. $m$ . For each region $[\eta]_{m}$ , the unique successor region is

$\blacksquare$

$\mathit{suc}([\eta]_{m})=[\eta]_{m}$ if $\eta(\texttt{x})>m$ for all $\texttt{x}\in\mathcal{X}$ ,
$\blacksquare$

$\mathit{suc}([\eta]_{m})=[\eta^{\prime}]_{m}$ iff there is $d\in\mathbb{R}^{\geq 0}$ such that $\eta{+}d=\eta^{\prime}$ , and $\eta{+}d^{\prime}\in[\eta]_{m}\cup[\eta^{\prime}]_{m}$ for all $0<d^{\prime}<d$ , and $[\eta]_{m}\not=[\eta^{\prime}]_{m}$ .

The second term defines the successor region of $[\eta]$ to be the first region that is entered if time passes from any $\eta^{\prime\prime}\in[\eta]$ , and the first term makes the successor region well-defined in regions where all clocks have values greater than $m$ . We call this region the maximal region.

5.2 The Untiming Construction

Let $\mathcal{X}$ be a set of clocks, let $\mathcal{Y}$ be a set of specification clocks. Let $\mathcal{T}_{t}=(\mathcal{S},\mathop{{\hbox{{$\mathrel{\mathop{\hbox to8.19447% pt{\rightarrowfill}}\limits}$}}}},s_{0},\lambda)$ be the tTS generated by the HORTA $t$ . Note that $\mathcal{S}\subseteq\{(v,\eta)\mid v\in T,\eta\models\iota(l{v})\}$ .

Let $\mathit{Prop},\Xi$ be the propositions, resp. clock constraints mentioned by $\varphi$ , and let $\mathcal{Y}$ be the specification clocks that $\varphi$ mentions. Define an (untimed) $\mu$ -calculus formula $\hat{\varphi}$ via

$\displaystyle\hat{p}$	$\displaystyle=p$	$\displaystyle\hat{X}$	$\displaystyle=X$
$\displaystyle\hat{\chi}$	$\displaystyle=\chi$	$\displaystyle\widehat{\neg\varphi^{\prime}}$	$\displaystyle=\neg\hat{\varphi^{\prime}}$
$\displaystyle\widehat{\varphi_{1}\vee\varphi_{2}}$	$\displaystyle=\hat{\varphi_{1}}\vee\hat{\varphi_{2}}$	$\displaystyle\widehat{\varphi_{1}\wedge\varphi_{2}}$	$\displaystyle=\hat{\varphi_{1}}\wedge\hat{\varphi_{2}}$
$\displaystyle\widehat{\varphi_{1}\rhd\varphi_{2}}$	$\displaystyle=\mu Z.\ (\hat{\varphi_{1}}\wedge\Diamond_{D}Z)\vee(\Diamond_{T}(% \mu Z^{\prime}.\ (\hat{\varphi_{1}}\wedge\Diamond_{D}Z^{\prime})\vee(\hat{% \varphi_{1}}\vee\hat{\varphi_{2}})))$	$\displaystyle\widehat{\texttt{z}.\ \varphi^{\prime}}$	$\displaystyle=\Diamond_{z}\hat{\varphi^{\prime}}$
$\displaystyle\widehat{\varphi_{1}\boxminus\varphi 2}$	$\displaystyle=\nu Z.\ (\hat{\varphi_{1}}\wedge\Box_{D}Z)\wedge(\Box_{T}(\nu Z^% {\prime}.\ (\hat{\varphi_{1}}\wedge\Box_{D}Z^{\prime})\wedge(\hat{\varphi_{1}}% \vee\hat{\varphi_{2}})))$
$\displaystyle\widehat{\mu X.\ \varphi^{\prime}}$	$\displaystyle=\mu X.\ \hat{\varphi^{\prime}}$	$\displaystyle\widehat{\nu X.\ \varphi^{\prime}}$	$\displaystyle=\nu X.\ \hat{\varphi^{\prime}}$

where the $Z,Z^{\prime}$ for the $\rhd$ and $\boxminus$ are fresh for each subformula. The semantics of the untimed modal operators are standard: $\llbracket\Diamond_{D}\psi\rrbracket_{\mathcal{T}}^{\alpha}=\{s\mid\text{ ex.% \ }s^{\prime}\in\llbracket\psi\rrbracket_{\mathcal{T}}^{\alpha}\text{ s.t.\ }s% \mathop{{\hbox{{$\mathrel{\mathop{\hbox to14.94824pt{\rightarrowfill}}\limits^% {D}}$}}}}s^{\prime}\}$ and similarly for $\Box_{D}$ and the other modalities. Note that this definition is for untimed transition systems.

Let $m$ be that largest integer in any location invariant or guard in $t$ or a clock constraint in $\varphi$ . Let $[\eta]$ denote $[\eta]_{m}$ from now on. Define a new (untimed) transition system with transitions $\{D,T\}\cup\{z\mid z\in\mathcal{Y}\}$ and propositions in $\mathit{Prop}\cup\Xi$ via $\mathcal{T}_{T}^{u}=(\mathcal{S}_{u},\mathop{{\hbox{{$\mathrel{\mathop{\hbox to% 8.19447pt{\rightarrowfill}}\limits}$}}}}_{u},s^{\prime}_{0},\lambda^{\prime})$ via

$\blacksquare$

$\mathcal{S}_{u}=\{(v,[\eta])\mid(v,\eta)\in\mathcal{S}\}$ ,
$\blacksquare$

$\mathop{{\hbox{{$\mathrel{\mathop{\hbox to8.19447pt{\rightarrowfill}}\limits}$% }}}}_{u}=\{(v,[\eta])\mathop{{\hbox{{$\mathrel{\mathop{\hbox to14.94824pt{% \rightarrowfill}}\limits^{D}}$}}}}(v,\mathit{suc}(\eta))\mid\mathit{suc}(\eta)% \models\iota(l(v))\}\cup\{(v,[\eta])\mathop{{\hbox{{$\mathrel{\mathop{\hbox to% 13.99413pt{\rightarrowfill}}\limits^{T}}$}}}}(vi,[\eta^{\prime}])\mid(v,\eta)% \mathop{{\hbox{{$\mathrel{\mathop{\hbox to8.19447pt{\rightarrowfill}}\limits}$% }}}}(vi,\eta^{\prime})\}\cup\{(v,[\eta])\mathop{{\hbox{{$\mathrel{\mathop{% \hbox to11.86943pt{\rightarrowfill}}\limits^{\texttt{z}}}$}}}}(v,[\eta]|_{% \texttt{z}})\mid\eta|_{\texttt{z}}\models\iota(l(v))\}$ ,
$\blacksquare$

$s^{\prime}_{0}=(\epsilon,[\eta_{0}])$ ,
$\blacksquare$

$\lambda^{\prime}((v,[\eta]))=\lambda(v,\eta)=\lambda(v)\cup\{\chi\in\Xi\mid% \eta\models\chi\}$ .

Finally, given a variable assignment $\alpha\colon\mathcal{V}\to 2^{\mathcal{S}}$ , define $\hat{\alpha}\colon\mathcal{V}\to 2^{\mathcal{S}^{\prime}}$ via $\hat{\alpha}(X)=\{(v,[\eta])\mid(v,\eta)\in\alpha(X)\}$ .

Proposition 7 ([2]).

For all subformulas $\psi$ of $\varphi$ , for all $(v,\eta)\in\mathcal{S}$ , and for all variable assignments $\alpha$ we have $(v,\eta)\in\llbracket\psi\rrbracket_{\mathcal{T}}^{\alpha}$ iff $(v,[\eta])\in\llbracket\hat{\psi}\rrbracket_{\mathcal{T}_{T}^{u}}^{\hat{\alpha}}$ .

Technically the proof in [2] is only for tTS defined via TA, not via HORTA. However, finiteness is not a crucial ingredient of the proof, and the region graph construction is very robust.

5.3 The Reduction

We have seen before that, on the region graph, the formula $\hat{\varphi}$ captures the semantics of $\varphi$ . We define an APT $\mathcal{P}_{\varphi}$ alongside the logic of $\hat{\varphi}$ , but based on the syntax of $\varphi$ itself. The reason for that is in the details of the translation of $\rhd$ and $\boxminus$ , where we have to make sure that the regions are visited one by one, but must also avoid excessive pointless delays. The states of $\mathcal{P}_{\varphi}$ will be the product of the set of subformulas of $\varphi$ and the set of regions in the region graph, plus some extra copies in some places. Transitions will follow the logic of subformulas in the first component, and pass through the regions as need be at formulas with real-time semantics, e.g., $\rhd,\boxminus$ .

As a preparation, let $\Sigma$ be the tree alphabet used in $t$ . Define $\Sigma^{\prime}=\Sigma\cup\{a_{\text{aux}}\mid a\in\Sigma\}$ where all the new tree constructors are unary. Let $m$ be the integer used for the region graph. The longest sequence of delay transitions that can be taken before reaching the maximal region is less than $k^{\prime}=|\mathcal{X}\cup\mathcal{Y}|\cdot 3\cdot m$ . Let $k$ be the length of the longest path in the syntax tree of $\varphi$ that contains no formulas of the form $\psi_{1}\rhd\psi_{2}$ or $\psi_{1}\boxminus\psi_{2}$ , including passing through fixpoint variables. This number exists due to guardedness. Write $\mathbf{k}$ for $2\cdot k^{\prime}+k$ .

Obtain a $\lambda Y$ term $\hat{t}$ from $t$ by replacing each occurrence of a tree constructor $a$ by $a_{\text{aux}}^{\mathbf{k}}\ a$ . i.e., by prepending it by a sequence of $\mathbf{k}$ many copies of $a_{\text{aux}}$ . These tree constructors give the yet-to-be-defined automaton enough space to (i) explicitly simulate delay transitions in the region graph by transitions reading $a_{\text{aux}}$ in the tree, and (ii) allow easy handling of the logic of subformulas by transitions without advancing in the tree proper.

Let $\mathcal{P}_{\varphi}=(Q,\Sigma^{\prime},\delta,q_{I},\Lambda)$ with the individual components defined as follows:

$\blacksquare$

$Q=\mathit{sub}(\varphi)\times\mathbb{R}^{\geq 0}/_{\simeq_{m}}\times\{0,1,2\}$ and $q_{I}=(\varphi,[\eta_{0}],0)$
$\blacksquare$
$\Lambda$ is defined inductively via the alternation index of a subformula of $\varphi$ . Let $\mathit{ai}(\psi)$ be defined inductively for formulas of the form $\mu X.\ \psi^{\prime}$ and $\nu x.\ \psi^{\prime}$ as follows:
- –
  
  For formulas of the form $\psi=\mu x.\ \psi^{\prime}$ set $\mathit{ai}(\psi)$ to the smallest even integer that is at least as big as $\mathit{ai}(\psi^{\prime\prime})$ for all subformulas $\psi^{\prime\prime}$ of $\psi$ , but at least $0$ .
- –
  
  For formulas of the form $\psi=\mu x.\ \psi^{\prime}$ set $\mathit{ai}(\psi)$ to the smallest odd integer that is at least as big as $\mathit{ai}(\psi^{\prime\prime})$ for all subformulas $\psi^{\prime\prime}$ of $\psi$ , but at least $1$ .
Fo other $\psi^{\prime}$ , set $\mathit{ai}(\psi)$ to $\mathit{ai}(\psi^{\prime})$ where $\psi^{\prime}$ is the first subformula of the form $\mu X.\ \psi^{\prime}$ or $\nu X.\ \psi^{\prime}$ on the path to the root in the syntax tree of ${\varphi}$ . Then $\Lambda((\psi,[\eta],i))=\mathit{ai}(\psi)$ .

Finally, $\delta$ is defined (for the non-modalities) as follows:

	$\displaystyle\delta((p,[\eta],0),a_{\text{aux}})$	$\displaystyle=\top\text{ if }p\in\lambda(a);\bot\text{ ow.}$
	$\displaystyle\delta((\neg p,[\eta],0),a_{\text{aux}})$	$\displaystyle=\bot\text{ if }p\in\lambda(a);\top\text{ ow.}$
	$\displaystyle\delta((\chi,[\eta],0),a_{\text{aux}})$	$\displaystyle=\top\text{ if }\eta\models\chi;\bot\text{ ow.}$
	$\displaystyle\delta((\neg\chi,[\eta],0),a_{\text{aux}})$	$\displaystyle=\bot\text{ if }\eta\not\models\chi;\top\text{ ow.}$
	$\displaystyle\delta((\psi_{1}\vee\psi_{2},[\eta],0),a_{\text{aux}})$	$\displaystyle=(\psi_{1},[\eta],0)\vee(\psi_{2},[\eta],0)$
	$\displaystyle\delta((\psi_{1}\wedge\psi_{2},[\eta],0),a_{\text{aux}})$	$\displaystyle=(\psi_{1},[\eta],0)\wedge(\psi_{2},[\eta],0)$
	$\displaystyle\delta((\mu X.\ \psi,[\eta],0),a_{\text{aux}})$	$\displaystyle=(\psi,[\eta],0)$
	$\displaystyle\delta((\nu X.\ \psi,[\eta],0),a_{\text{aux}})$	$\displaystyle=(\psi[\eta],0)$
	$\displaystyle\delta((X,[\eta],0),a_{\text{aux}})$	$\displaystyle=(\mathit{fp}(X),[\eta],0)$
	$\displaystyle\delta((\texttt{z}.\ \psi,[\eta],0),a_{\text{aux}})$	$\displaystyle=(\psi,[\eta\|_{\{z\}}],0)\text{ if }\eta\|_{\{\texttt{z}\}}\models% \iota(a)$

The intuition here is that the acceptance game simply follows the logic of the subformula in question. The transitions for $\rhd$ are

	$\displaystyle\delta((\psi_{1}\rhd\psi_{2},[\eta],0),a_{\text{aux}})$	$\displaystyle=(\psi_{1},[\eta],0)\wedge(\psi_{1}\rhd\psi_{2},[\eta],1)\text{ % if }\mathit{suc}([\eta]_{m})\not\models\iota(a)\text{ or }[\eta]\text{ is max.}$
	$\displaystyle\delta((\psi_{1}\rhd\psi_{2},[\eta],0),a_{\text{aux}})$	$\displaystyle=(\psi_{1},[\eta],0)\wedge((\psi_{1}\rhd\psi_{2},[\eta],1)\vee(% \psi_{1}\rhd\psi_{2},\mathit{suc}([\eta]),0))$
		$\displaystyle\qquad\qquad\qquad\text{ if }\mathit{suc}([\eta]_{m})\models\iota% (a)\text{ and }[\eta]\text{ is not max.}$
	$\displaystyle\delta((\psi_{1}\rhd\psi_{2},[\eta],1),a_{\text{aux}})$	$\displaystyle=(\psi_{1}\rhd\psi_{2},[\eta],1)$
	$\displaystyle\delta((\psi_{1}\rhd\psi_{2},[\eta],1),a)$	$\displaystyle=\bigvee_{j\in\{0,\dotsc,\mathit{ar}(a),\mathit{trns}_{j}(a)=(% \chi,R),\eta\models\chi}\!\!\!\!\!\!\!\!(q_{\top}^{i},(\psi_{1}\rhd\psi_{2},[% \eta\|_{R}],2),q_{\top}^{\mathit{ar}(a)-i-1})$
	$\displaystyle\delta((\psi_{1}\rhd\psi_{2},[\eta],2),a_{\text{aux}}$	$\displaystyle=\bot\text{ if }\eta\not\models\iota(a)$
	$\displaystyle\delta((\psi_{1}\rhd\psi_{2},[\eta],2),a_{\text{aux}})$	$\displaystyle=(\psi_{2},[\eta],0)\text{ if }\eta\models\iota(a)\text{ and }% \mathit{suc}([\eta]_{m})\not\models\iota(a)\text{ or }[\eta]\text{ is max.}$
	$\displaystyle\delta((\psi_{1}\rhd\psi_{2},[\eta],2),a_{\text{aux}})$	$\displaystyle=(\psi_{1},[\eta],2)\wedge((\psi_{2},[\eta],0)\vee(\psi_{1}\rhd% \psi_{2},\mathit{suc}([\eta]),2))$
		$\displaystyle\qquad\qquad\text{ if }\eta\models\iota(a)\text{ and }\mathit{suc% }([\eta]_{m})\models\iota(a)\text{ and }[\eta]\text{ is not max.}$

We omit the clauses for $\psi_{1}\boxminus\psi_{2}$ as they are dual to those for $\psi_{1}\rhd\psi_{2}$ . The logic of a temporal next follows three phases: a delay, a discrete transition, and then another delay. First, if the last component of the state is $0$ , $\exists$ advances to successor regions of she so desires, and if this is possible. Then, if the last component is $1$ , the sequence of $a_{\text{aux}}$ is consumed and an actual transition happens at $a$ , with an immediate check for satisfaction of the location invariant. Then, $\exists$ can delay further if she so desires. After she is done with this, the APT tracks $\psi_{2}$ .

Lemma 8.

Let $\mathcal{T}_{\hat{t}}$ be the tree generated by $\hat{t}$ . Then $\mathcal{P}_{\varphi}$ accepts $\mathcal{T}_{\hat{t}}$ iff $(\epsilon,\eta_{0})\in\llbracket\varphi\rrbracket_{\mathcal{T}_{t}}$ .

It is immediate that $\hat{t}$ is tail-recursive if $t$ is. Moreover, one can show that $\mathcal{P}_{\varphi}$ is a baAPT if $\varphi$ has bounded alternation.

Theorem 9.

The model-checking problem for order- $k$ HORTA against $T_{\mu}$ formulas is in $(k+1)$ -EXPTIME. For tail-recursive order- $k$ -HORTA and bounded-alternation formulas, the problem is in $k$ -EXPSPACE.

Proof.

Note that $\mathcal{P}_{\varphi}$ is exponential in the input, since it contains the region graph in its state space. Since the model-checking problem for order- $k$ HORS is $k$ -EXPTIME-complete [20], we obtain the result. For the tail-recursive case, we obtain the claim via Prop. 3. $\hfill\blacktriangleleft$

6 Matching Lower Bounds

We now show that the model-checking problem for bounded-alternation $T_{\mu}$ formulas against trees generated by order- $1$ HORTA is EXPSPACE-hard, via a reduction from the corridor tiling problem (see below). The general case of $k$ -EXPSPACE-hardness for model-checking order- $k$ HORTA is left for a future publication. The proof uses an idea from [12, 11].

6.1 Tiling Problems

A tiling system is a $\mathcal{K}=(K,H,V,k_{I},t_{\square},t_{F})$ where $K$ is a finite set of tiles, $H,V\subseteq K\times K$ are the horizontal and vertical matching relations, and $k_{I},k_{\square},k_{F}$ are the initial, blank and final tiles. The corridor tiling problem consumes as input a tiling system $\mathcal{K}$ and some $n\in\mathbb{N}$ encoded unarily. It asks whether there is a sequence $\rho_{0},\dotsc,\rho_{m-1}$ , where each of the $\rho_{i}$ is a $K$ -word of length $2^{n}$ that satisfies the following:

$\blacksquare$

$\rho_{0}=k_{I}k_{\square}\dotsb k_{\square}$ ,
$\blacksquare$

for each $0\leq i\leq m-1$ , and $0\leq j<2^{n}-1$ , we have $(\rho_{i}(j),\rho_{i}(j+1))\in H$ ,
$\blacksquare$

for each $0\leq i\leq m-2$ and $0\leq j\leq 2^{n}-1$ , we have $(\rho_{i}(j),\rho_{i+1}(j))\in V$ , and
$\blacksquare$

$\rho_{m-1}(0)=k_{F}$ ,

where $\rho_{i}(j)$ denotes the $j$ th tile in $\rho_{i}$ . We call the $i$ th word in this solution the $i$ th row.

Proposition 10 ([23, 15]).

The corridor tiling problem is EXPSPACE-hard.

6.2 Encoding Rows

Let $\mathcal{K}=(K,H,V,k_{I},k_{\square},k_{F})$ be a tiling system, and assume that $K$ is ordered, e.g., via $K=\{k_{0},\dotsc,k_{m-1}\}$ for $m=|K|$ . W.l.o.g. let $k_{I}=k_{0},k_{\square}=k_{1}$ . A row candidate is a $K$ -word of length $2^{n}$ . Such a row candidate is a row if it satisfies the horizontal matching. Row candidates are also lexicographically ordered. Given a row candidate $\rho$ , we obtain the lexicographically next one $\rho^{\prime}$ by setting $\rho^{\prime}(j)=\rho(j)$ if there is $j<j^{\prime}<2^{n}$ s.t. $\rho(j)\not=k_{m-1}$ , and if $\rho(j)=k_{i}$ and $\rho(j^{\prime})=k_{m-1}$ for all $j<j^{\prime}<2^{n}$ , then $\rho^{\prime}(j)=k_{i+1\pmod{m}}$ .

We now encode rows and row candidates into trees generated by $\lambda Y$ terms over a timed tree alphabet (i.e., HORTA), and, for each $k\in K$ , define a $T_{\mu}$ formula that checks whether a given tile in a the row encoded by such a tree is $k$ . These formulas are mutually recursive, but the recursion is guarded by the designated proposition $p_{\text{sf}}$ (cf. Sec. 4). The HORTA has one clock x. A node $v$ in the underlying tree encodes a row $\rho$ if, for each $0\leq i<2^{n}$ , $(v,\texttt{x}\mapsto i)\in\llbracket\psi_{k}\rrbracket_{\mathcal{T}_{T}}$ iff $k=\rho(i)$ . Here, $\mathcal{T}_{T}$ is the tTS defined by the HORTA.

Let $\mathit{Prop}=\{p_{I},p_{\square},p_{\text{sf}}\}$ and let $\Sigma=\{a_{nxt}^{1},a_{rw}^{2},b_{I}^{1},b_{\square}^{1}\}$ with arities indicated by superscripts. Let $\mathit{trns}_{0}(b_{I})=\mathit{trns}_{0}(b_{\square})=(\texttt{z}=1,\{% \texttt{z}\})$ . Set $\lambda^{-1}(p_{I})=\{b_{I}\}$ and $\lambda^{-1}(p_{\square})=\{b_{\square}\}$ and $\lambda^{-1}(p_{\text{sf}})=\{a_{nxt}\}$ , where $p_{\text{sf}}$ is the designated proposition from the definition of tail recursion/bounded alternation. We write $\rhd_{i}\psi$ for $\texttt{z}.\ \texttt{t\!t}\rhd(\texttt{z}=i\wedge\psi)$ , and $\boxminus_{i}\psi$ for $\texttt{z}.\ \texttt{t\!t}\boxminus(\texttt{z}=i\wedge\psi)$ . Consider the $\lambda Y$ terms

init

\displaystyle=b_{I}\ (YF.\ b_{\square}\ F)\qquad

\displaystyle\qquad\texttt{next}\ t

\displaystyle=a_{nxt}(YF.\ a_{rw}\ F\ t).

The first one defines a tree with $b_{I}$ as the root and then an infinite sequence of $b_{\square}$ after that. The other consumes a tree and returns a tree that contains $a_{nxt}$ as the root, and then below it an infinite leftward sequence of $a_{rw}$ that each contain $t$ as their right son. All rows and row candidates we work with are obtained from init via repeated application of next.

Now consider the mutually recursive $T_{\mu}$ formulas

	$\displaystyle\psi_{k_{0}}$	$\displaystyle=p_{I}\vee\big(\rhd_{0}(p_{\text{sf}}\wedge\psi_{k_{m-1}}\wedge% \rhd_{0}\mu X.\ \neg p_{\text{sf}}\wedge\psi_{k_{m-1}}\wedge(\texttt{x}=2^{n}-% 1\vee\rhd_{1}X))\big)$
		$\displaystyle\qquad\;\vee\big(\rhd_{0}(p_{\text{sf}}\wedge\psi_{k_{0}}\wedge% \rhd_{0}\mu X.\ \neg p_{\text{sf}}\wedge(\texttt{x}\leq 2^{n}-1\wedge\neg\psi_% {k_{m-1}}\vee\rhd_{1}X))\big)$
	$\displaystyle\psi_{k_{1}}$	$\displaystyle=p_{\square}\vee\big(\rhd_{0}(p_{\text{sf}}\wedge\psi_{k_{0}}% \wedge\rhd_{0}\mu X.\ \neg p_{\text{sf}}\wedge\psi_{k_{m-1}}\wedge(\texttt{x}=% 2^{n}-1\vee\rhd_{1}X))\big)$
		$\displaystyle\qquad\;\,\vee\big(\rhd_{1}(p_{\text{sf}}\wedge\psi_{k_{0}}\wedge% \rhd_{0}\mu X.\ \neg p_{\text{sf}}\wedge(\texttt{x}\leq 2^{n}-1\wedge\neg\psi_% {k_{m-1}}\vee\rhd_{1}X))\big)$
	$\displaystyle\psi_{k_{i+2}}$	$\displaystyle=\qquad\;\big(\rhd_{0}(p_{\text{sf}}\wedge\psi_{k_{i+1}}\wedge% \rhd_{0}\mu X.\ \neg p_{\text{sf}}\wedge\psi_{k_{m-1}}\wedge(\texttt{x}=2^{n}-% 1\vee\rhd_{1}X))\big)$
		$\displaystyle\qquad\;\,\vee\big(\rhd_{0}(p_{\text{sf}}\wedge\psi_{k_{i+2}}% \wedge\rhd_{0}\mu X.\ \neg p_{\text{sf}}\wedge(\texttt{x}\leq 2^{n}-1\wedge% \neg\psi_{k_{m-1}}\vee\rhd_{1}X))\big).$

The idea is that encoding a tile is signaled by a proposition (only for $k_{I},k_{\square}$ ), or it holds due to the recursive characterization of the lexicographic successor, applied recursively until the propositional base case is reached. This is done by traversing along $a_{rw}$ (used to let time elapse in increments of $1$ ) or $a_{nxt}$ (from $\texttt{next}\ t$ to $t$ ). Given a row candidate $\rho$ , let $\mathtt{next}^{i}(\rho)$ be the lexicographically $i$ th successor of $\rho$ modulo $2^{n}$ .

Lemma 11.

The tree generated by init encodes the initial row. Given a tree that encodes a row candidate $\rho$ , the tree generated by $\textup{{next}}^{i}\ t$ encodes $\mathtt{next}^{i}(\rho)$ .

6.3 The Reduction

Extend $\Sigma$ by $\{a_{v}^{1},a_{h}^{1}\}$ and $\mathit{Prop}$ by $\{p_{h},p_{v}\}$ with $\lambda^{-1}(p_{v})=\{a_{v}\},\lambda^{-1}(p_{h})=\{a_{h}\}$ . Now consider the $\lambda Y$ terms

	$\displaystyle\texttt{horiz}\ t$	$\displaystyle=a_{h}(YF.\ a_{rw}\ F\ t)$
	$\displaystyle\texttt{vert}\ t\ t^{\prime}$	$\displaystyle=(YF.\ a_{v}\ (a_{v}\ (F\ t\ t^{\prime}))\ (a_{rw}\ t\ (a_{rw}(t^% {\prime}\ t^{\prime})))$

and the $T_{\mu}$ formulas

	$\displaystyle\psi_{\texttt{horiz}}$	$\displaystyle=\rhd_{0}\Big(p_{h}\wedge\big(\bigwedge_{(k,k^{\prime})\notin H}% \nu X.\ (\psi_{k}\rightarrow\neg\psi_{k^{\prime}})\wedge((\texttt{x}=2^{n}-1% \vee\rhd_{1}(\neg p_{\text{sf}}\wedge X)))\big)\Big)$
	$\displaystyle\psi_{\texttt{vert}}$	$\displaystyle=\bigwedge_{(k,k^{\prime})\notin V}\nu X.\ (\rhd_{0}\psi_{k}% \rightarrow\neg\rhd_{0}(\neg p_{\text{sf}}\wedge\rhd_{0}\neg p_{\text{sf}}% \wedge\psi_{k^{\prime}})$
		$\displaystyle\qquad\qquad\qquad\qquad\qquad\qquad\quad\wedge((\texttt{x}=2^{n}% -1\vee\rhd_{0}(p_{v}\wedge\rhd_{1}\neg p_{\text{sf}}\wedge X))))$

Lemma 12.

$\psi_{\texttt{horiz}}$ holds on the tree generated by $\textup{{horiz}}\ t$ iff $t$ encodes a row, i.e., if the row candidate it encodes satisfies horizontal matching. $\psi_{\texttt{vert}}$ holds on the tree generated by $\textup{{vert}}\ t\ t^{\prime}$ iff the rows encoded by $t$ and $t^{\prime}$ match vertically.

Finally, extend $\mathit{Prop}$ by $\{p_{\vee},p_{\wedge},p_{f}\}$ and $\Sigma$ by $\{a_{\vee}^{2},a_{\wedge}^{2},a_{f}^{1}\}$ with $\lambda^{-1}(p_{\vee})=\{a_{\vee}\}$ and $\lambda^{-1}(p_{\wedge})=\{a_{\wedge}\}$ and $\lambda^{-1}(p_{f})=\{a_{f}\}$ . Consider the $\lambda Y$ terms

	$\displaystyle\texttt{check}\ t\ t^{\prime}$	$\displaystyle=a_{\wedge}\ (\texttt{horiz}\ t^{\prime})\ (\texttt{vert}\ t\ t^{% \prime})$
	$\displaystyle\texttt{exists}\ t\ t^{\prime}$	$\displaystyle=YF.\ a_{\vee}\ (a_{\wedge}(\texttt{check}\ t\ t^{\prime})\ (G\ t% ^{\prime}))\ (F\ t\ (\texttt{next}\ t^{\prime}))$
	tiling	$\displaystyle=\big(YG.\ \lambda t.\ a_{\vee}\ (a_{f}\ t)\ (\texttt{exists}\ t% \ \texttt{init})\big)\ \texttt{init}$

and the $T_{\mu}$ formulas

	$\displaystyle\psi_{\texttt{final}}$	$\displaystyle=\psi_{k_{1}}$
	$\displaystyle\psi_{\texttt{chk}}$	$\displaystyle=\boxminus_{0}((p_{h}\wedge\psi_{\texttt{horiz}})\vee(p_{v}\wedge% \psi_{\texttt{vert}}))$
	$\displaystyle\psi_{\texttt{srch}}$	$\displaystyle=\mu X_{\texttt{srch}}.\ \rhd_{0}\big(p_{f}\wedge\psi_{\texttt{% final}})$
		$\displaystyle\qquad\qquad\big(p_{\vee}\wedge\mu Y.\ \rhd_{0}(p_{\wedge}\wedge(% \boxminus_{0}(p_{\wedge}\wedge\psi_{\texttt{check}}\vee(p_{\vee}\wedge X)))% \vee(p_{\vee}\wedge Y))\big)$

Lemma 13.

$\psi_{\texttt{final}}$ holds on the tree generated by $\textup{{final}}\ t$ iff $t$ encodes a final row. $\psi_{\texttt{check}}$ holds on the tree generated by $\textup{{check}}\ t\ t^{\prime}$ if (i) $t$ encodes a row and (ii) $t$ and $t^{\prime}$ match vertically.

Finally, $\psi_{\texttt{srch}}$ holds on the tree generated by tiling iff $\mathcal{K}$ has a solution.

It is not hard to show that tiling is tail recursive, but not obvious that $\psi_{\texttt{srch}}$ has bounded alternation.

Lemma 14.

The $\lambda Y$ term tiling is tail recursive. The $T_{\mu}$ fomula $\psi_{\texttt{srch}}$ is bounded-alternation and of polynomial size in $\mathcal{K}$ .

This yields the following theorem.

Theorem 15.

The model-checking problem of tail-recursive HORTA against bounded-alternation $T_{\mu}$ formulas is EXPSPACE-hard.

Proof.

By Prop. 10, the corridor tiling problem is EXPSPACE-hard. By Lem. 13, an instance of the corridor tiling problem has a solution iff $\psi_{\texttt{srch}}$ holds on the tree generated by tiling. Since by Lem. 14, the former is bounded-alternation and the latter is tail-recursive, and both are of polynomial size in $\mathcal{K}$ , this constitutes a polynomial-time reduction. $\hfill\blacktriangleleft$

7 Conclusion

We have refined the notion of Real-Time Recursion Schemes [3] into that of HORTA, and established matching upper bounds for the model-checking problem. We have also shown that the model-checking problem for HORTA becomes easier by half an exponential in the tail-recursive setting. The lower bound has been established for the order- $1$ case, but we conjecture that it can be extended to all orders. The corridor tiling problem needs to be replaced by an exponential version [15], and the encoding of a row needs to be lifted from a tree to a function that consumes a tree, and returns a tree etc., see e.g., [3, 9].

References

[1] Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler. Scheduling with timed automata. Theor. Comput. Sci., 354(2):272–300, 2006. doi:10.1016/J.TCS.2005.11.018.
[2] Luca Aceto and François Laroussinie. Is your model checker on time? on the complexity of model checking for timed modal logics. J. Log. Algebraic Methods Program., 52-53:7–51, 2002. doi:10.1016/S1567-8326(02)00022-X.
[3] Eric Alsmann and Florian Bruse. Real-time higher-order recursion schemes. In Pietro Sala, Michael Sioutis, and Fusheng Wang, editors, 31st International Symposium on Temporal Representation and Reasoning, TIME 2024, October 28-30, 2024, Montpellier, France, volume 318 of LIPIcs, pages 16:1–16:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.TIME.2024.16.
[4] Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, 1993. doi:10.1006/inco.1993.1024.
[5] Rajeev Alur and David L. Dill. Automata for modeling real-time systems. In Mike Paterson, editor, Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, UK, July 16-20, 1990, Proceedings, volume 443 of Lecture Notes in Computer Science, pages 322–335. Springer, 1990. doi:10.1007/BFB0032042.
[6] C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008.
[7] Massimo Benerecetti, Stefano Minopoli, and Adriano Peron. Analysis of timed recursive state machines. In 2010 17th International Symposium on Temporal Representation and Reasoning, pages 61–68, 2010. doi:10.1109/TIME.2010.10.
[8] Ahmed Bouajjani, Rachid Echahed, and Riadh Robbana. On the automatic verification of systems with continuous variables and unbounded discrete data structures. In Hybrid Systems II, pages 64–85, Berlin, Heidelberg, 1995. Springer-Verlag.
[9] Florian Bruse. Space-efficient model-checking of higher-order recursion schemes. In Shankaranarayanan Krishna, Sriram Sankaranarayanan, and Ashutosh Trivedi, editors, Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Denver, CO, USA, January 20-21, 2025, Proceedings, Part I, volume 15529 of Lecture Notes in Computer Science, pages 29–51. Springer, 2025. doi:10.1007/978-3-031-82700-6_2.
[10] Florian Bruse, Oliver Friedmann, and Martin Lange. On guarded transformation in the modal $\mu$ -calculus. Log. J. IGPL, 23(2):194–216, 2015. doi:10.1093/JIGPAL/JZU030.
[11] Florian Bruse and Martin Lange. The tail-recursive fragment of timed recursive CTL. Inf. Comput., 294:105084, 2023. doi:10.1016/J.IC.2023.105084.
[12] Florian Bruse, Martin Lange, and Étienne Lozes. Space-efficient fragments of higher-order fixpoint logic. In Matthew Hague and Igor Potapov, editors, Reachability Problems - 11th International Workshop, RP 2017, London, UK, September 7-9, 2017, Proceedings, volume 10506 of Lecture Notes in Computer Science, pages 26–41. Springer, 2017. doi:10.1007/978-3-319-67089-8_3.
[13] Lorenzo Clemente and Slawomir Lasota. Timed pushdown automata revisited. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 738–749. IEEE Computer Society, 2015. doi:10.1109/LICS.2015.73.
[14] Werner Damm. The IO- and oi-hierarchies. Theor. Comput. Sci., 20:95–207, 1982. doi:10.1016/0304-3975(82)90009-3.
[15] Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. doi:10.1017/CBO9781139236119.
[16] Martijn Hendriks and Marcel Verhoef. Timed automata based analysis of embedded system architectures. In Proceedings 20th IEEE International Parallel & Distributed Processing Symposium, pages 8–pp. IEEE, 2006.
[17] Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Inf. Comput., 111(2):193–244, 1994. doi:10.1006/INCO.1994.1045.
[18] Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205–222. Springer, 2002. doi:10.1007/3-540-45931-6_15.
[19] Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 179–188. IEEE Computer Society, 2009. doi:10.1109/LICS.2009.29.
[20] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81–90. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.38.
[21] Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Information and Compututation, 239:340–355, 2014. doi:10.1016/J.IC.2014.07.012.
[22] Ashutosh Trivedi and Dominik Wojtczak. Recursive timed automata. In Ahmed Bouajjani and Wei-Ngan Chin, editors, Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings, volume 6252 of Lecture Notes in Computer Science, pages 306–324. Springer, 2010. doi:10.1007/978-3-642-15643-4_23.
[23] P. van Emde Boas. The convenience of tilings. In A. Sorbi, editor, Complexity, Logic, and Recursion Theory, volume 187 of Lecture notes in pure and applied mathematics, pages 331–363. Marcel Dekker, Inc., 1997.

Appendix A Additional Material

A.1 An example of a HORTA

Consider the example of a delivery truck that waits at a station to leave for its deliveries. It can either leave, or stay at the station, for example because the driver’s mandatory break is not over. Every time the option is presented and the truck stays, however, it is loaded with an additional parcel that will need to be delivered during the next tour of the truck. Waiting at the station takes between $1$ and $2$ time units, and the driver has to wait for at least $5$ minutes. Delivering each parcel will take between $2$ or $3$ minutes. We ask: is it possible to complete the mandatory waiting time of $5$ minutes, but end up with a tour that can be completed in $10$ minutes or less?

We model this as follows: Let $\{\texttt{stat}^{2},\texttt{par}^{1},\texttt{end}^{0}\}$ be a tree alphabet with arities as indicated. Add a unique proposition $p_{\text{end}}$ with $\lambda(p_{\text{end}})=\{\texttt{end}\}$ .

Consider the $\lambda Y$ term $t=\big(YF.\ \lambda x.\ \texttt{stat}\ x\ (F\ (\texttt{par}\ x))\big)\ \texttt% {end}$ . Note that this term is tail recursive. It defines an infinite tree of the following form, which encodes the different ways waiting and delivering can play out:

We now convert the $\lambda Y$ term $t$ into a HORTA by setting $\iota(\texttt{stat})=\texttt{x}\leq 2$ , $\iota(\texttt{par})=\texttt{x}\leq 3$ and $\mathit{trns}_{0}(\texttt{stat})=(\texttt{z}\geq 5,\{\texttt{z}\})$ , $\mathit{trns}_{1}(\texttt{stat})=(\texttt{x}\geq 1,\{\texttt{x}\}),\mathit{% trns}_{0}(\texttt{par})=(\texttt{x}\geq 2,\{\texttt{x}\})$ .

The intuition here is that clock x is used to measure waiting times at the station and delivery times of the individual parcels, while clock z is used to measure the break, and the overall delivery time.

We can visualize the tree like this:

Here, location invariants are drawn next to the nodes, and pairs of transition guards and resets drawn next to the edges. The proposition $p_{\text{end}}$ appears next to the final nodes.

A $T_{\mu}$ formula that verifies the property above is $\mu X.\ (p\wedge\texttt{z}\leq 10)\vee(\texttt{t\!t}\rhd X)$ . Note that the dependence between the waiting times and the overall delivery time cannot be incorporated into a finite-state TA due to the strictly nonregular behavior of loading additional parcels. Also note that this formula has bounded boolean alternation. Since the term that gives riseto the HORTA above is also tail recursive, a problem like this can be verified more efficiently, since the

In a real-time recursion scheme (cf. [3]), such a situation could also be modeled, but less naturally. Such a real-time recursion scheme generated trees where the tree constructors are simply annotated by plain intervals, which roughly signals how much time it takes to process such a constructor. No connection to individual clocks is made by the tree. Instead, the tree generated by such a real-time scheme is to be verified against a pair of a TA and an APT, with some synchronization between the two. This means that a significant part of the behavior of the system that is being modeled must be added to this automaton, and great care must be taken to synchronize the APT and he TA. Conversely, in a HORTA, the system being modeled manifests itself almost exclusively in the (recursive) TA, as can be seen above. The formulas that specify the desired property can then be comparatively simple. In the case above, a simple reachability property suffices.

[bib.bib1] [1] Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler. Scheduling with timed automata. Theor. Comput. Sci., 354(2):272–300, 2006. doi:10.1016/J.TCS.2005.11.018.

[bib.bib2] [2] Luca Aceto and François Laroussinie. Is your model checker on time? on the complexity of model checking for timed modal logics. J. Log. Algebraic Methods Program., 52-53:7–51, 2002. doi:10.1016/S1567-8326(02)00022-X.

[bib.bib3] [3] Eric Alsmann and Florian Bruse. Real-time higher-order recursion schemes. In Pietro Sala, Michael Sioutis, and Fusheng Wang, editors, 31st International Symposium on Temporal Representation and Reasoning, TIME 2024, October 28-30, 2024, Montpellier, France, volume 318 of LIPIcs, pages 16:1–16:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.TIME.2024.16.

[bib.bib4] [4] Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, 1993. doi:10.1006/inco.1993.1024.

[bib.bib5] [5] Rajeev Alur and David L. Dill. Automata for modeling real-time systems. In Mike Paterson, editor, Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, UK, July 16-20, 1990, Proceedings, volume 443 of Lecture Notes in Computer Science, pages 322–335. Springer, 1990. doi:10.1007/BFB0032042.

[bib.bib6] [6] C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008.

[bib.bib7] [7] Massimo Benerecetti, Stefano Minopoli, and Adriano Peron. Analysis of timed recursive state machines. In 2010 17th International Symposium on Temporal Representation and Reasoning, pages 61–68, 2010. doi:10.1109/TIME.2010.10.

[bib.bib8] [8] Ahmed Bouajjani, Rachid Echahed, and Riadh Robbana. On the automatic verification of systems with continuous variables and unbounded discrete data structures. In Hybrid Systems II, pages 64–85, Berlin, Heidelberg, 1995. Springer-Verlag.

[bib.bib9] [9] Florian Bruse. Space-efficient model-checking of higher-order recursion schemes. In Shankaranarayanan Krishna, Sriram Sankaranarayanan, and Ashutosh Trivedi, editors, Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Denver, CO, USA, January 20-21, 2025, Proceedings, Part I, volume 15529 of Lecture Notes in Computer Science, pages 29–51. Springer, 2025. doi:10.1007/978-3-031-82700-6_2.

[bib.bib10] [10] Florian Bruse, Oliver Friedmann, and Martin Lange. On guarded transformation in the modal $\mu$ -calculus. Log. J. IGPL, 23(2):194–216, 2015. doi:10.1093/JIGPAL/JZU030.

[bib.bib11] [11] Florian Bruse and Martin Lange. The tail-recursive fragment of timed recursive CTL. Inf. Comput., 294:105084, 2023. doi:10.1016/J.IC.2023.105084.

[bib.bib12] [12] Florian Bruse, Martin Lange, and Étienne Lozes. Space-efficient fragments of higher-order fixpoint logic. In Matthew Hague and Igor Potapov, editors, Reachability Problems - 11th International Workshop, RP 2017, London, UK, September 7-9, 2017, Proceedings, volume 10506 of Lecture Notes in Computer Science, pages 26–41. Springer, 2017. doi:10.1007/978-3-319-67089-8_3.

[bib.bib13] [13] Lorenzo Clemente and Slawomir Lasota. Timed pushdown automata revisited. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 738–749. IEEE Computer Society, 2015. doi:10.1109/LICS.2015.73.

[bib.bib14] [14] Werner Damm. The IO- and oi-hierarchies. Theor. Comput. Sci., 20:95–207, 1982. doi:10.1016/0304-3975(82)90009-3.

[bib.bib15] [15] Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. doi:10.1017/CBO9781139236119.

[bib.bib16] [16] Martijn Hendriks and Marcel Verhoef. Timed automata based analysis of embedded system architectures. In Proceedings 20th IEEE International Parallel & Distributed Processing Symposium, pages 8–pp. IEEE, 2006.

[bib.bib17] [17] Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Inf. Comput., 111(2):193–244, 1994. doi:10.1006/INCO.1994.1045.

[bib.bib18] [18] Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205–222. Springer, 2002. doi:10.1007/3-540-45931-6_15.

[bib.bib19] [19] Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 179–188. IEEE Computer Society, 2009. doi:10.1109/LICS.2009.29.

[bib.bib20] [20] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81–90. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.38.

[bib.bib21] [21] Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Information and Compututation, 239:340–355, 2014. doi:10.1016/J.IC.2014.07.012.

[bib.bib22] [22] Ashutosh Trivedi and Dominik Wojtczak. Recursive timed automata. In Ahmed Bouajjani and Wei-Ngan Chin, editors, Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings, volume 6252 of Lecture Notes in Computer Science, pages 306–324. Springer, 2010. doi:10.1007/978-3-642-15643-4_23.

[bib.bib23] [23] P. van Emde Boas. The convenience of tilings. In A. Sorbi, editor, Complexity, Logic, and Recursion Theory, volume 187 of Lecture notes in pure and applied mathematics, pages 331–363. Marcel Dekker, Inc., 1997.

Higher-Order Timed Automata and Tail Recursion

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

2.1 Trees and Automata

2.2 Higher-Order Recursion Schemes

Types and Terms.

Semantics.

2.3 Timed Automata

2.4 The Timed 𝝁-Calculus

Proposition 1 ([2]).

2.5 Tail Recursion

Bounded-Alternation Parity Automata.

Tail-Recursion for 𝝀⁢𝒀 Terms.

Definition 2.

Proposition 3 ([9]).

3 Higher-Order Recursive Timed Automata

Definition 4.

Definition 5.

4 Tail Recursion

5 Upper Bounds for Model-Checking

5.1 The Region Abstraction

Definition 6.

5.2 The Untiming Construction

Proposition 7 ([2]).

5.3 The Reduction

Lemma 8.

Theorem 9.

Proof.

6 Matching Lower Bounds

6.1 Tiling Problems

Proposition 10 ([23, 15]).

6.2 Encoding Rows

Lemma 11.

6.3 The Reduction

Lemma 12.

Lemma 13.

Lemma 14.

Theorem 15.

Proof.

7 Conclusion

References

Appendix A Additional Material

A.1 An example of a HORTA

2.4 The Timed $\mu$ -Calculus

Tail-Recursion for $\lambda Y$ Terms.