cs.FL

arXiv:2307.08780v2 Announce Type: replace Abstract: Discounting the influence of future events is a key paradigm in economics and it is widely used in computer-science models, such as games, Markov decision processes (MDPs), reinforcement learning, and automata. While a single game or MDP may allow for several different discount factors, discounted-sum automata (NDAs) were only studied with respect to a single discount factor. It is known that every class of NDAs with an integer as the discount factor has good computational properties: It is closed under determinization and under the algebraic operations min, max, addition, and subtraction, and there are algorithms for its basic decision problems, such as automata equivalence and containment. Extending the integer discount factor to an arbitrary rational number, loses most of these good properties. We define and analyze nondeterministic discounted-sum automata in which each transition can have a different integral discount factor (integral NMDAs). We show that integral NMDAs with an arbitrary choice of discount factors are not closed under determinization and under algebraic operations and that their containment problem is undecidable. We then define and analyze a restricted class of integral NMDAs, which we call tidy NMDAs, in which the choice of discount factors depends on the prefix of the word read so far. Among their special cases are NMDAs that correlate discount factors to actions (alphabet letters) or to the elapsed time. We show that for every function $\theta$ that defines the choice of discount factors, the class of $\theta$-NMDAs enjoys all of the above good properties of NDAs with a single integral discount factor, as well as the same complexity of the required decision problems. Tidy NMDAs are also as expressive as deterministic integral NMDAs with an arbitrary choice of discount factors.

arXiv:2411.07741v2 Announce Type: replace Abstract: Complex Cyber-Physical System (CPS) such as Unmanned Aerial System (UAS) got rapid development these years, but also became vulnerable to GPS spoofing, packets injection, buffer-overflow and other malicious attacks. Ensuring the behaviors of UAS always keeping secure no matter how the environment changes, would be a prospective direction for UAS security. This paper aims at introducing a pattern-based framework to describe the security properties of UAS, and presenting a reactive synthesis-based approach to implement the automatic generation of secure UAS controller. First, we study the operating mechanism of UAS and construct a high-level model consisting of actuator and monitor. Besides, we analyze the security threats of UAS from the perspective of hardware, software and cyber physics, and then summarize the corresponding specification patterns of security properties with LTL formulas. With the UAS model and security specification patterns, automatons for controller can be constructed by General Reactivity of Rank 1 (GR(1)) synthesis algorithm, which is a two-player game process between Unmanned Aerial Vehicle (UAV) and its environment. Finally, we experimented under the Ardupilot simulation platform to test the effectiveness of our method.

arXiv:2411.19906v2 Announce Type: replace-cross Abstract: L-systems can be made to model and create simulations of many biological processes, such as plant development. Finding an L-system for a given process is typically solved by hand, by experts, in a massively time-consuming process. It would be significant if this could be done automatically from data, such as from sequences of images. In this paper, we are interested in inferring a particular type of L-system, deterministic context-free L-system (D0L-system) from a sequence of strings. We introduce the characteristic graph of a sequence of strings, which we then utilize to translate our problem (inferring D0L-system) in polynomial time into the maximum independent set problem (MIS) and the SAT problem. After that, we offer a classical exact algorithm and an approximate quantum algorithm for the problem.

arXiv:2501.00364v1 Announce Type: new Abstract: Reward machines (RMs) are an effective approach for addressing non-Markovian rewards in reinforcement learning (RL) through finite-state machines. Traditional RMs, which label edges with propositional logic formulae, inherit the limited expressivity of propositional logic. This limitation hinders the learnability and transferability of RMs since complex tasks will require numerous states and edges. To overcome these challenges, we propose First-Order Reward Machines ($\texttt{FORM}$s), which use first-order logic to label edges, resulting in more compact and transferable RMs. We introduce a novel method for $\textbf{learning}$ $\texttt{FORM}$s and a multi-agent formulation for $\textbf{exploiting}$ them and facilitate their transferability, where multiple agents collaboratively learn policies for a shared $\texttt{FORM}$. Our experimental results demonstrate the scalability of $\texttt{FORM}$s with respect to traditional RMs. Specifically, we show that $\texttt{FORM}$s can be effectively learnt for tasks where traditional RM learning approaches fail. We also show significant improvements in learning speed and task transferability thanks to the multi-agent learning framework and the abstraction provided by the first-order language.

arXiv:2501.00784v1 Announce Type: cross Abstract: In 2009 Benoit Cloitre introduced a certain self-generating sequence $$(a_n)_{n\geq 1} = 1, 1, 2, 1, 1, 1, 1, 2, 1, 1, 2, 1, 1, 2, 2, \ldots,$$ with the property that the sum of the terms appearing in the $n$'th run equals twice the $n$'th term of the sequence. We give a connection between this sequence and the paperfolding sequence, and then prove Cloitre's conjecture about the density of $1$'s appearing in $(a_n)_{n \geq 1}$.

arXiv:2302.06420v3 Announce Type: replace Abstract: We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.

arXiv:2412.17930v1 Announce Type: cross Abstract: The paperfolding sequences form an uncountable class of infinite sequences over the alphabet $\{ -1, 1 \}$ that describe the sequence of folds arising from iterated folding of a piece of paper, followed by unfolding. In this note we observe that the sequence of run lengths in such a sequence, as well as the starting and ending positions of the $n$'th run, is $2$-synchronized and hence computable by a finite automaton. As a specific consequence, we obtain the recent results of Bunder, Bates, and Arnold, in much more generality, via a different approach. We also prove results about the critical exponent and subword complexity of these run-length sequences.

arXiv:2412.18425v1 Announce Type: cross Abstract: Two finite words are k-binomially equivalent if each subword (i.e., subsequence) of length at most k occurs the same number of times in both words. The k-binomial complexity of an infinite word is a function that maps the integer $n\geq 0$ to the number of k-binomial equivalence classes represented by its factors of length n. The Thue--Morse (TM) word and its generalization to larger alphabets are ubiquitous in mathematics due to their rich combinatorial properties. This work addresses the k-binomial complexities of generalized TM words. Prior research by Lejeune, Leroy, and Rigo determined the k-binomial complexities of the 2-letter TM word. For larger alphabets, work by L\"u, Chen, Wen, and Wu determined the 2-binomial complexity for m-letter TM words, for arbitrary m, but the exact behavior for $k\geq 3$ remained unresolved. They conjectured that the k-binomial complexity function of the m-letter TM word is eventually periodic with period $m^k$. We resolve the conjecture positively by deriving explicit formulae for the k-binomial complexity functions for any generalized TM word. We do this by characterizing k-binomial equivalence among factors of generalized TM words. This comprehensive analysis not only solves the open conjecture, but also develops tools such as abelian Rauzy graphs.

arXiv:2402.17000v2 Announce Type: replace Abstract: Opacity is a general framework modeling security properties of systems interacting with a passive attacker. Initial-and-final-state opacity (IFO) generalizes the classical notions of opacity, such as current-state opacity and initial-state opacity. In IFO, the secret is whether the system evolved from a given initial state to a given final state or not. There are two algorithms for IFO verification. One arises from a trellis-based state estimator, which builds a semigroup of binary relations generated by the events of the automaton, and the other is based on the reduction to language inclusion. The time complexity of both algorithms is bounded by a super-exponential function, and it is a challenging open problem to find a faster algorithm or to show that no faster algorithm exists. We discuss the lower-bound time complexity for both general and special cases, and use extensive benchmarks to compare the existing algorithms.

arXiv:2412.16560v1 Announce Type: new Abstract: The piecewise complexity $h(u)$ of a word is the minimal length of subwords needed to exactly characterise $u$. Its piecewise minimality index $\rho(u)$ is the smallest length $k$ such that $u$ is minimal among its order-$k$ class $[u]_k$ in Simon's congruence. We initiate a study of these two descriptive complexity measures. Among other results we provide efficient algorithms for computing $h(u)$ and $\rho(u)$ for a given word $u$.

arXiv:2412.16612v1 Announce Type: new Abstract: Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. The central algorithmic challenge in VASS is the reachability problem: is there a run from a given starting state and counter values to a given target state and counter values? When the input is encoded in binary, reachability is computationally intractable: even in dimension one, it is NP-hard. In this paper, we comprehensively characterise the tractability border of the problem when the input is encoded in unary. For our main result, we prove that reachability is NP-hard in unary encoded 3-VASS, even when structure is heavily restricted to be a simple linear path scheme. This improves upon a recent result of Czerwi\'nski and Orlikowski (2022), in both the number of counters and expressiveness of the considered model, as well as answers open questions of Englert, Lazi\'c, and Totzke (2016) and Leroux (2021). The underlying graph structure of a simple linear path scheme (SLPS) is just a path with self-loops at each node. We also study the exceedingly weak model of computation that is SPLS with counter updates in {-1,0,+1}. Here, we show that reachability is NP-hard when the dimension is bounded by O(\alpha(k)), where \alpha is the inverse Ackermann function and k bounds the size of the SLPS. We complement our result by presenting a polynomial-time algorithm that decides reachability in 2-SLPS when the initial and target configurations are specified in binary. To achieve this, we show that reachability in such instances is well-structured: all loops, except perhaps for a constant number, are taken either polynomially many times or almost maximally. This extends the main result of Englert, Lazi\'c, and Totzke (2016) who showed the problem is in NL when the initial and target configurations are specified in unary.

arXiv:2412.16793v1 Announce Type: new Abstract: The parity index problem of tree automata asks, given a regular tree language L, what is the least number of priorities of a nondeterministic parity tree automaton that recognises L. This is a long-standing open problem, also known as the Mostowski or Rabin-Mostowski index problem, of which only a few sub-cases and variations are known to be decidable. In a significant step, Colcombet and L\"oding reduced the problem to the uniform universality of distance-parity automata. In this brief note, we present a similar result, with a simplified proof, based on on the games in Lehtinen's quasipolynomial algorithm for parity games. We define an extended version of these games, which we call parity transduction games, which take as parameters a parity index J and an integer bound N. We show that the language of a guidable automaton A is recognised by a nondeterministic automaton of index J if and only if there is a bound N such that the parity transduction game with parameters J and N captures membership of the language, that is, for all trees t, Eve wins the parity transduction game on the acceptance parity game of t in A if and only in t is in L(A).

arXiv:2307.09776v2 Announce Type: replace Abstract: Recently interest has increased in applying reactive synthesis to more practical richer-than-Boolean domains. One of the major challenges in this area is to establish when certain repeating behaviour terminates in a desired state when the number of steps is unbounded. This isolated problem, by itself, is already undecidable, and forms part of the overall difficulty of this kind of synthesis tasks. Relatively successful approaches exist for deterministic games with at most B{\"u}chi conditions. Our contribution goes beyond, being the first effective approach for solving symbolic synthesis problems with full LTL objectives, based on novel liveness refinements guided by the underlying game. Our CEGAR-based approach relies on a sound boolean abstraction of the problem, spuriousness checking of abstract counterstrategies through invariant checking, and extracting fresh safety or liveness properties of the concrete game from counterexamples. The latter are used to refine the abstraction, which is used to re-attempt synthesis. Our discrete synthesis tool outperforms the state-of-the-art on LIA benchmarks from literature. We also introduce benchmarks that are out of scope for all other approaches.

arXiv:2412.15799v1 Announce Type: new Abstract: Timed automata are a widely used formalism for specifying discrete-state/continuous-time behaviors of time-critical reactive systems. Concerning the fundamental verification problem of comparing a candidate implementation against a specification, both given as timed automata over the same alphabet, it has been shown that timed trace equivalence is undecidable, whereas timed bisimulation equivalence is decidable. The corresponding decidability proof utilizes region graphs, a finite but often unnecessarily space-consuming characterization of timed automata semantics. In practice, most verification tools use zone graphs instead, a symbolic and, on average, more space-efficient representation of timed automata semantics. However, zone graphs only provide sound results for those verification tasks being reducible to plain location-reachability problems thus being too imprecise for timed-bisimilarity checking. In particular, potentially distinctive effects of, by definition invisible, clock resets on the subsequent branching behaviors in a timed run may be abstracted away in a zone graph representation if this does not harm global reachability properties. As a consequence, to the best of our knowledge, no practical tool is currently available for automated timed-bisimilarity checking. In this paper, we propose a new representation of timed automata semantics to enable sound and complete timed bisimilarity checking, yet still guaranteeing a finite representation. To this end, we extend zone graphs by so-called virtual clocks to memorize previous delays, which is usually not possible due to clock resets. Our zone-based construction is, on average, significantly smaller than the corresponding region-graph representation. We also present experimental results gained from applying our tool implementation to TA models, which are frequently used in the evaluation of TA analysis techniques.