Models of iterated computation, such as (completely) iterative monads, often
depend on a notion of guardedness, which guarantees unique solvability of
recursive equations and requires roughly that recursive calls happen only under
certain guarding operations. On the other hand, many models of iteration do
admit unguarded iteration. Solutions are then no longer unique, and in general
not even determined as least or greatest fixpoints, being instead governed by
quasi-equational axioms. Monads that support unguarded iteration in this sense
are called (complete) Elgot monads. Here, we propose to equip (Kleisli
categories of) monads with an abstract notion of guardedness and then require
solvability of abstractly guarded recursive equations; examples of such
abstractly guarded pre-iterative monads include both iterative monads and Elgot
monads, the latter by deeming any recursive definition to be abstractly
guarded. Our main result is then that Elgot monads are precisely the
iteration-congruent retracts of abstractly guarded iterative monads, the latter
being defined as admitting unique solutions of abstractly guarded recursive
equations; in other words, models of unguarded iteration come about by
quotienting models of guarded iteration.
We show that the class of chordal claw-free graphs admits LREC$_=$-definable
canonization. LREC$_=$ is a logic that extends first-order logic with counting
by an operator that allows it to formalize a limited form of recursion. This
operator can be evaluated in logarithmic space. It follows that there exists a
logarithmic-space canonization algorithm, and therefore a logarithmic-space
isomorphism test, for the class of chordal claw-free graphs. As a further
consequence, LREC$_=$ captures logarithmic space on this graph class. Since
LREC$_=$ is contained in fixed-point logic with counting, we also obtain that
fixed-point logic with counting captures polynomial time on the class of
chordal claw-free graphs.
We consider the action of a linear subspace $U$ of $\{0,1\}^n$ on the set of
AC$^0$ formulas with inputs labeled by literals in the set $\{X_1,\overline
X_1,\dots,X_n,\overline X_n\}$, where an element $u \in U$ acts on formulas by
transposing the $i$th pair of literals for all $i \in [n]$ such that $u_i=1$. A
formula is {\em $U$-invariant} if it is fixed by this action. For example,
there is a well-known recursive construction of depth $d+1$ formulas of size
$O(n{\cdot}2^{dn^{1/d}})$ computing the $n$-variable PARITY function; these
formulas are easily seen to be $P$-invariant where $P$ is the subspace of
even-weight elements of $\{0,1\}^n$. In this paper we establish a nearly
matching $2^{d(n^{1/d}-1)}$ lower bound on the $P$-invariant depth $d+1$
formula size of PARITY. Quantitatively this improves the best known
$\Omega(2^{\frac{1}{84}d(n^{1/d}-1)})$ lower bound for {\em unrestricted} depth
$d+1$ formulas, while avoiding the use of the switching lemma. More generally,
for any linear subspaces $U \subset V$, we show that if a Boolean function is
$U$-invariant and non-constant over $V$, then its $U$-invariant depth $d+1$
formula size is at least $2^{d(m^{1/d}-1)}$ where $m$ is the minimum Hamming
weight of a vector in $U^\bot \setminus V^\bot$.
We establish zero-one laws and convergence laws for monadic second-order
logic (MSO) (and, a fortiori, first-order logic) on a number of interesting
graph classes. In particular, we show that MSO obeys a zero-one law on the
class of connected planar graphs, the class of connected graphs of tree-width
at most $k$ and the class of connected graphs excluding the $k$-clique as a
minor. In each of these cases, dropping the connectivity requirement leads to a
class where the zero-one law fails but a convergence law for MSO still holds.
We prove coherence theorems for Frobenius pseudomonoids and snakeorators in
monoidal bicategories. As a consequence we obtain a 3d notation for proofs in
nonsymmetric multiplicative linear logic, with a geometrical notion of
equivalence, and without the need for a global correctness criterion or
thinning links. We argue that traditional proof nets are the 2d projections of
these 3d diagrams.
We introduce a new setting where a population of agents, each modelled by a
finite-state system, are controlled uniformly: the controller applies the same
action to every agent. The framework is largely inspired by the control of a
biological system, namely a population of yeasts, where the controller may only
change the environment common to all cells. We study a synchronisation problem
for such populations: no matter how individual agents react to the actions of
the controller, the controller aims at driving all agents synchronously to a
target state. The agents are naturally represented by a non-deterministic
finite state automaton (NFA), the same for every agent, and the whole system is
encoded as a 2-player game. The first player (Controller) chooses actions, and
the second player (Agents) resolves non-determinism for each agent. The game
with m agents is called the m -population game. This gives rise to a
parameterized control problem (where control refers to 2 player games), namely
the population control problem: can Controller control the m-population game
for all m in N whatever Agents does?
Let $b$ be an integer strictly greater than $1$. Each set of nonnegative
integers is represented in base $b$ by a language over $\{0, 1, \dots, b -
1\}$. The set is said to be $b$-recognisable if it is represented by a regular
language. It is known that ultimately periodic sets are $b$-recognisable, for
every base $b$, and Cobham's theorem implies the converse: no other set is
$b$-recognisable in every base $b$.
We consider the following decision problem: let $S$ be a set of nonnegative
integers that is $b$-recognisable, given as a finite automaton over $\{0,1,
\dots, b - 1\}$, is $S$ periodic? Honkala showed in 1986 that this problem is
decidable. Later on, Leroux used in 2005 the convention to write number
representations with the least significant digit first (LSDF), and designed a
quadratic algorithm to solve a more general problem.
We use here LSDF convention as well and give a structural description of the
minimal automata that accept periodic sets. Then, we show that it can be
verified in linear time if a minimal automaton meets this description. In
general, this yields a $O(b \log(n))$ procedure to decide whether an automaton
with $n$ states accepts an ultimately periodic set of nonnegative integers.
It has been known since Ehrhard and Regnier's seminal work on the Taylor
expansion of $\lambda$-terms that this operation commutes with normalization:
the expansion of a $\lambda$-term is always normalizable and its normal form is
the expansion of the Böhm tree of the term. We generalize this result to the
non-uniform setting of the algebraic $\lambda$-calculus, i.e.
$\lambda$-calculus extended with linear combinations of terms. This requires us
to tackle two difficulties: foremost is the fact that Ehrhard and Regnier's
techniques rely heavily on the uniform, deterministic nature of the ordinary
$\lambda$-calculus, and thus cannot be adapted; second is the absence of any
satisfactory generic extension of the notion of Böhm tree in presence of
quantitative non-determinism, which is reflected by the fact that the Taylor
expansion of an algebraic $\lambda$-term is not always normalizable. Our
solution is to provide a fine grained study of the dynamics of
$\beta$-reduction under Taylor expansion, by introducing a notion of reduction
on resource vectors, i.e. infinite linear combinations of resource
$\lambda$-terms. The latter form the multilinear fragment of the differential
$\lambda$-calculus, and resource vectors are the target of the Taylor expansion
of $\lambda$-terms. We show the reduction of resource vectors contains the
image of any $\beta$-reduction step, from which we deduce that Taylor expansion
and normalization commute on the nose. We moreover identify a class […]
A cyclic proof system, called CLKID-omega, gives us another way of
representing inductive definitions and efficient proof search. The 2005 paper
by Brotherston showed that the provability of CLKID-omega includes the
provability of LKID, first order classical logic with inductive definitions in
Martin-Löf's style, and conjectured the equivalence. The equivalence has been
left an open question since 2011. This paper shows that CLKID-omega and LKID
are indeed not equivalent. This paper considers a statement called 2-Hydra in
these two systems with the first-order language formed by 0, the successor, the
natural number predicate, and a binary predicate symbol used to express
2-Hydra. This paper shows that the 2-Hydra statement is provable in
CLKID-omega, but the statement is not provable in LKID, by constructing some
Henkin model where the statement is false.
We introduce a parametrized version of the Wadge game for functions and show
that each lower cone in the Weihrauch degrees is characterized by such a game.
These parametrized Wadge games subsume the original Wadge game, the eraser and
backtrack games as well as Semmes's tree games. In particular, we propose that
the lower cones in the Weihrauch degrees are the answer to Andretta's question
on which classes of functions admit game characterizations.
We then discuss some applications of such parametrized Wadge games. Using
machinery from Weihrauch reducibility theory, we introduce games characterizing
every (transfinite) level of the Baire hierarchy via an iteration of a pruning
derivative on countably branching trees.
We study proof techniques for bisimilarity based on unique solution of
equations. We draw inspiration from a result by Roscoe in the denotational
setting of CSP and for failure semantics, essentially stating that an equation
(or a system of equations) whose infinite unfolding never produces a divergence
has the unique-solution property. We transport this result onto the operational
setting of CCS and for bisimilarity. We then exploit the operational approach
to: refine the theorem, distinguishing between different forms of divergence;
derive an abstract formulation of the theorems, on generic LTSs; adapt the
theorems to other equivalences such as trace equivalence, and to preorders such
as trace inclusion. We compare the resulting techniques to enhancements of the
bisimulation proof method (the `up-to techniques'). Finally, we study the
theorems in name-passing calculi such as the asynchronous $\pi$-calculus, and
use them to revisit the completeness part of the proof of full abstraction of
Milner's encoding of the $\lambda$-calculus into the $\pi$-calculus for
Lévy-Longo Trees.
We investigate powerspace constructions on topological spaces, with a
particular focus on the category of quasi-Polish spaces. We show that the upper
and lower powerspaces commute on all quasi-Polish spaces, and show more
generally that this commutativity is equivalent to the topological property of
consonance. We then investigate powerspace constructions on the open set
lattices of quasi-Polish spaces, and provide a complete characterization of how
the upper and lower powerspaces distribute over the open set lattice
construction.
In the context of abstract coinduction in complete lattices, the notion of
compatible function makes it possible to introduce enhancements of the
coinduction proof principle. The largest compatible function, called the
companion, subsumes most enhancements and has been proved to enjoy many good
properties. Here we move to universal coalgebra, where the corresponding notion
is that of a final distributive law. We show that when it exists, the final
distributive law is a monad, and that it coincides with the codensity monad of
the final sequence of the given functor. On sets, we moreover characterise this
codensity monad using a new abstract notion of causality. In particular, we
recover the fact that on streams, the functions definable by a distributive law
or GSOS specification are precisely the causal functions. Going back to
enhancements of the coinductive proof principle, we finally obtain that any
causal function gives rise to a valid up-to-context technique.
We present a categorical construction for modelling causal structures within
a general class of process theories that include the theory of classical
probabilistic processes as well as quantum theory. Unlike prior constructions
within categorical quantum mechanics, the objects of this theory encode
fine-grained causal relationships between subsystems and give a new method for
expressing and deriving consequences for a broad class of causal structures. We
show that this framework enables one to define families of processes which are
consistent with arbitrary acyclic causal orderings. In particular, one can
define one-way signalling (a.k.a. semi-causal) processes, non-signalling
processes, and quantum $n$-combs. Furthermore, our framework is general enough
to accommodate recently-proposed generalisations of classical and quantum
theory where processes only need to have a fixed causal ordering locally, but
globally allow indefinite causal ordering.
To illustrate this point, we show that certain processes of this kind, such
as the quantum switch, the process matrices of Oreshkov, Costa, and Brukner,
and a classical three-party example due to Baumeler, Feix, and Wolf are all
instances of a certain family of processes we refer to as $\textrm{SOC}_n$ in
the appropriate category of higher-order causal processes. After defining these
families of causal structures within our framework, we give derivations of
their operational behaviour using simple, diagrammatic axioms.
Automata with monitor counters, where the transitions do not depend on
counter values, and nested weighted automata are two expressive
automata-theoretic frameworks for quantitative properties. For a well-studied
and wide class of quantitative functions, we establish that automata with
monitor counters and nested weighted automata are equivalent. We study for the
first time such quantitative automata under probabilistic semantics. We show
that several problems that are undecidable for the classical questions of
emptiness and universality become decidable under the probabilistic semantics.
We present a complete picture of decidability for such automata, and even an
almost-complete picture of computational complexity, for the probabilistic
questions we consider.
Propositional team logic is the propositional analog to first-order team
logic. Non-classical atoms of dependence, independence, inclusion, exclusion
and anonymity can be expressed in it, but for all atoms except dependence only
exponential translations are known. In this paper, we systematically compare
their succinctness in the existential fragment, where the splitting disjunction
only occurs positively, and in full propositional team logic with unrestricted
negation. By introducing a variant of the Ehrenfeucht-Fra\"{i}ssé game
called formula size game into team logic, we obtain exponential lower bounds in
the existential fragment for all atoms. In the full fragment, we present
polynomial upper bounds also for all atoms.
We consider the problem of checking whether a proposed invariant $\varphi$
expressed in first-order logic with quantifier alternation is inductive, i.e.
preserved by a piece of code. While the problem is undecidable, modern SMT
solvers can sometimes solve it automatically. However, they employ powerful
quantifier instantiation methods that may diverge, especially when $\varphi$ is
not preserved. A notable difficulty arises due to counterexamples of infinite
size.
This paper studies Bounded-Horizon instantiation, a natural method for
guaranteeing the termination of SMT solvers. The method bounds the depth of
terms used in the quantifier instantiation process. We show that this method is
surprisingly powerful for checking quantified invariants in uninterpreted
domains. Furthermore, by producing partial models it can help the user diagnose
the case when $\varphi$ is not inductive, especially when the underlying reason
is the existence of infinite counterexamples.
Our main technical result is that Bounded-Horizon is at least as powerful as
instrumentation, which is a manual method to guarantee convergence of the
solver by modifying the program so that it admits a purely universal invariant.
We show that with a bound of 1 we can simulate a natural class of
instrumentations, without the need to modify the code and in a fully automatic
way. We also report on a prototype implementation on top of Z3, which we used
to verify several examples by Bounded-Horizon of bound 1.
Completion is one of the most studied techniques in term rewriting and
fundamental to automated reasoning with equalities. In this paper we present
new correctness proofs of abstract completion, both for finite and infinite
runs. For the special case of ground completion we present a new proof based on
random descent. We moreover extend the results to ordered completion, an
important extension of completion that aims to produce ground-complete
presentations of the initial equations. We present new proofs concerning the
completeness of ordered completion for two settings. Moreover, we revisit and
extend results of Métivier concerning canonicity of rewrite systems. All
proofs presented in the paper have been formalized in Isabelle/HOL.
Quantitative extensions of parity games have recently attracted significant
interest. These extensions include parity games with energy and payoff
conditions as well as finitary parity games and their generalization to parity
games with costs. Finitary parity games enjoy a special status among these
extensions, as they offer a native combination of the qualitative and
quantitative aspects in infinite games: The quantitative aspect of finitary
parity games is a quality measure for the qualitative aspect, as it measures
the limit superior of the time it takes to answer an odd color by a larger even
one. Finitary parity games have been extended to parity games with costs, where
each transition is labeled with a nonnegative weight that reflects the costs
incurred by taking it. We lift this restriction and consider parity games with
costs with arbitrary integer weights.
We show that solving such games is in NP $\cap$ coNP, the signature
complexity for games of this type. We also show that the protagonist has
finite-state winning strategies, and provide tight pseudo-polynomial bounds for
the memory he needs to win the game. Naturally, the antagonist may need
infinite memory to win. Moreover, we present tight bounds on the quality of
winning strategies for the protagonist.
Furthermore, we investigate the problem of determining, for a given threshold
$b$, whether the protagonist has a strategy of quality at most $b$ and show
this problem to be EXPTIME-complete. The protagonist […]
We present the first polynomial time algorithm to learn nontrivial classes of
languages of infinite trees. Specifically, our algorithm uses membership and
equivalence queries to learn classes of $\omega$-tree languages derived from
weak regular $\omega$-word languages in polynomial time. The method is a
general polynomial time reduction of learning a class of derived $\omega$-tree
languages to learning the underlying class of $\omega$-word languages, for any
class of $\omega$-word languages recognized by a deterministic Büchi
acceptor. Our reduction, combined with the polynomial time learning algorithm
of Maler and Pnueli [1995] for the class of weak regular $\omega$-word
languages yields the main result. We also show that subset queries that return
counterexamples can be implemented in polynomial time using subset queries that
return no counterexamples for deterministic or non-deterministic finite word
acceptors, and deterministic or non-deterministic Büchi $\omega$-word
acceptors.
A previous claim of an algorithm to learn regular $\omega$-trees due to
Jayasrirani, Begam and Thomas [2008] is unfortunately incorrect, as shown in
Angluin [2016].
We present new results on realtime alternating, private alternating, and
quantum alternating automaton models. Firstly, we show that the emptiness
problem for alternating one-counter automata on unary alphabets is undecidable.
Then, we present two equivalent definitions of realtime private alternating
finite automata (PAFAs). We show that the emptiness problem is undecidable for
PAFAs. Furthermore, PAFAs can recognize some nonregular unary languages,
including the unary squares language, which seems to be difficult even for some
classical counter automata with two-way input. Regarding quantum finite
automata (QFAs), we show that the emptiness problem is undecidable both for
universal QFAs on general alphabets, and for alternating QFAs with two
alternations on unary alphabets. On the other hand, the same problem is
decidable for nondeterministic QFAs on general alphabets. We also show that the
unary squares language is recognized by alternating QFAs with two alternations.
In the context of ontology-mediated querying with description logics (DLs),
we study the data complexity of queries in which selected predicates can be
closed (OMQCs). We provide a non-uniform analysis, aiming at a classification
of the complexity into tractable and non-tractable for ontologies in the
lightweight DLs DL-Lite and EL, and the expressive DL ALCHI. At the level of
ontologies, we prove a dichotomy between FO-rewritable and coNP-complete for
DL-Lite and between PTime and coNP-complete for EL. The meta problem of
deciding tractability is proved to be in PTime. At the level of OMQCs, we show
that there is no dichotomy (unless NP equals PTime) if both concept and role
names can be closed. If only concept names can be closed, we tightly link the
complexity of query evaluation to the complexity of surjective CSPs. We also
identify a class of OMQCs based on ontologies formulated in DL-Lite that are
guaranteed to be tractable and even FO-rewritable.
Most of the physical processes arising in nature are modeled by either
ordinary or partial differential equations. From the point of view of analog
computability, the existence of an effective way to obtain solutions of these
systems is essential. A pioneering model of analog computation is the General
Purpose Analog Computer (GPAC), introduced by Shannon as a model of the
Differential Analyzer and improved by Pour-El, Lipshitz and Rubel, Costa and
Graça and others. Its power is known to be characterized by the class of
differentially algebraic functions, which includes the solutions of initial
value problems for ordinary differential equations. We address one of the
limitations of this model, concerning the notion of approximability, a
desirable property in computation over continuous spaces that is however absent
in the GPAC. In particular, the Shannon GPAC cannot be used to generate
non-differentially algebraic functions which can be approximately computed in
other models of computation. We extend the class of data types using networks
with channels which carry information on a general complete metric space $X$;
for example $X=C(R,R)$, the class of continuous functions of one real (spatial)
variable. We consider the original modules in Shannon's construction
(constants, adders, multipliers, integrators) and we add \emph{(continuous or
discrete) limit} modules which have one input and one output. We then define an
L-GPAC to be a network built with $X$-stream channels and […]
This paper is the fourth of a series exposing a systematic combinatorial
approach to Girard's Geometry of Interaction (GoI) program. The GoI program
aims at obtaining particular realisability models for linear logic that
accounts for the dynamics of cut-elimination. This fourth paper tackles the
complex issue of defining exponential connectives in this framework. For that
purpose, we use the notion of \emph{graphings}, a generalisation of graphs
which was defined in earlier work. We explain how to define a GoI for
Elementary Linear Logic (ELL) with second-order quantification, a sub-system of
linear logic that captures the class of elementary time computable functions.
We introduce the fermionic ZW calculus, a string-diagrammatic language for
fermionic quantum computing (FQC). After defining a fermionic circuit model, we
present the basic components of the calculus, together with their
interpretation, and show how the main physical gates of interest in FQC can be
represented in our language. We then list our axioms, and derive some
additional equations. We prove that the axioms provide a complete equational
axiomatisation of the monoidal category whose objects are systems of finitely
many local fermionic modes (LFMs), with maps that preserve or reverse the
parity of states, and the tensor product as monoidal product. We achieve this
through a procedure that rewrites any diagram in a normal form. As an example,
we show how the statistics of a fermionic Mach-Zehnder interferometer can be
calculated in the diagrammatic language. We conclude by giving a diagrammatic
treatment of the dual-rail encoding, a standard method in optical quantum
computing used to perform universal quantum computation.
In this article we provide effective characterisations of regular languages
of infinite trees that belong to the low levels of the Wadge hierarchy. More
precisely we prove decidability for each of the finite levels of the hierarchy;
for the class of the Boolean combinations of open sets $BC(\Sigma_1^0)$ (i.e.
the union of the first $\omega$ levels); and for the Borel class $\Delta_2^0$
(i.e. for the union of the first $\omega_1$ levels).
The purpose of this paper is to provide a construction to model
shared-variable systems using higher-dimensional automata which is
compositional in the sense that the parallel composition of completely
independent systems is modeled by the standard tensor product of HDAs and
nondeterministic choice is represented by the coproduct.
We look at characterizing which formulas are expressible in rich decidable
logics such as guarded fixpoint logic, unary negation fixpoint logic, and
guarded negation fixpoint logic. We consider semantic characterizations of
definability, as well as effective characterizations. Our algorithms revolve
around a finer analysis of the tree-model property and a refinement of the
method of moving back and forth between relational logics and logics over
trees.
Pomset logic introduced by Retoré is an extension of linear logic with a
self-dual noncommutative connective. The logic is defined by means of
proof-nets, rather than a sequent calculus. Later a deep inference system BV
was developed with an eye to capturing Pomset logic, but equivalence of system
has not been proven up to now. As for a sequent calculus formulation, it has
not been known for either of these logics, and there are convincing arguments
that such a sequent calculus in the usual sense simply does not exist for them.
In an on-going work on semantics we discovered a system similar to Pomset
logic, where a noncommutative connective is no longer self-dual. Pomset logic
appears as a degeneration, when the class of models is restricted. Motivated by
these semantic considerations, we define in the current work a semicommutative
multiplicative linear logic}, which is multiplicative linear logic extended
with two nonisomorphic noncommutative connectives (not to be confused with very
different Abrusci-Ruet noncommutative logic). We develop a syntax of proof-nets
and show how this logic degenerates to Pomset logic. However, a more
interesting problem than just finding yet another noncommutative logic is to
find a sequent calculus for this logic. We introduce decorated sequents, which
are sequents equipped with an extra structure of a binary relation of
reachability on formulas. We define a decorated sequent calculus for
semicommutative logic and prove that it is cut-free, […]
The parameterized model-checking problem for a class of first-order sentences
(queries) asks to decide whether a given sentence from the class holds true in
a given relational structure (database); the parameter is the length of the
sentence. We study the parameterized space complexity of the model-checking
problem for queries with a bounded number of variables. For each bound on the
quantifier alternation rank the problem becomes complete for the corresponding
level of what we call the tree hierarchy, a hierarchy of parameterized
complexity classes defined via space bounded alternating machines between
parameterized logarithmic space and fixed-parameter tractable time. We observe
that a parameterized logarithmic space model-checker for existential bounded
variable queries would allow to improve Savitch's classical simulation of
nondeterministic logarithmic space in deterministic space $O(\log^2n)$.
Further, we define a highly space efficient model-checker for queries with a
bounded number of variables and bounded quantifier alternation rank. We study
its optimality under the assumption that Savitch's Theorem is optimal.
Game theory provides a well-established framework for the analysis of
concurrent and multi-agent systems. The basic idea is that concurrent processes
(agents) can be understood as corresponding to players in a game; plays
represent the possible computation runs of the system; and strategies define
the behaviour of agents. Typically, strategies are modelled as functions from
sequences of system states to player actions. Analysing a system in such a
setting involves computing the set of (Nash) equilibria in the concurrent game.
However, we show that, with respect to the above model of strategies (arguably,
the "standard" model in the computer science literature), bisimilarity does not
preserve the existence of Nash equilibria. Thus, two concurrent games which are
behaviourally equivalent from a semantic perspective, and which from a logical
perspective satisfy the same temporal logic formulae, may nevertheless have
fundamentally different properties (solutions) from a game theoretic
perspective. Our aim in this paper is to explore the issues raised by this
discovery. After illustrating the issue by way of a motivating example, we
present three models of strategies with respect to which the existence of Nash
equilibria is preserved under bisimilarity. We use some of these models of
strategies to provide new semantic foundations for logics for strategic
reasoning, and investigate restricted scenarios where bisimilarity can be shown
to preserve the existence of Nash […]
We consider the model-checking problem for freeze LTL on one-counter automata
(OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to
store different counter values of a run in registers so that they can be
compared with one another. As the model-checking problem is undecidable in
general, we focus on the flat fragment of freeze LTL, in which the usage of the
freeze quantifier is restricted. In a previous work, Lechner et al. showed that
model checking for flat freeze LTL on OCA with binary encoding of counter
updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem
is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in
unary or binary. Like Lechner et al., we rely on a reduction to the
reachability problem in OCA with parameterized tests (OCA(P)). The new aspect
is that we simulate OCA(P) by alternating two-way automata over words. This
implies an exponential upper bound on the parameter values that we exploit
towards an NP algorithm for reachability in OCA(P) with unary updates. We
obtain our main result as a corollary. As another application, relying on a
reduction by Bundala and Ouaknine, one obtains an alternative proof of the
known fact that reachability in closed parametric timed automata with one
parametric clock is in NEXPTIME.