Searcharxiv⌕ Search

arXiv subjects

Alexander Rabinovich

Publications and source records attributed to Alexander Rabinovich.

18 recordsLinked to original sources
arXiv2026

Decidability of MSO Reparameterization over Countable Chains

Interpretations are a fundamental tool in mathematical logic, allowing structures to be encoded within other structures via logical definitions. We study $\MSO$ \emph{multidimensional point interpretations}, where elements of an interpreted structure are represented by tuples of elements of the host structure, and address the problem of simplifying such interpretations by reducing their representation dimension. To formalize simplification, we use the notion of \emph{reparameterization}. Our main result shows that, over the class of countable labelled linear orders, it is decidable whether a given $\MSO$ formula admits a $d$-dimensional reparameterization. As a consequence, every interpretation whose domain admits such a reparameterization is equivalent to a $d$-dimensional point interpretation.

cs.LO↗
arXiv2025

The Church Synthesis Problem over Continuous Time

The Church Problem asks for the construction of a procedure which, given a logical specification A(I,O) between input omega-strings I and output omega-strings O, determines whether there exists an operator F that implements the specification in the sense that A(I, F(I)) holds for all inputs I. Buchi and Landweber provided a procedure to solve the Church problem for MSO specifications and operators computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time domain of the non-negative reals. We show that in the continuous time domain there are phenomena which are very different from the canonical discrete time domain of the natural numbers.

cs.LO↗
arXiv2025

Synthesis of Infinite State Systems

The classical Church synthesis problem, solved by Buchi and Landweber, treats the synthesis of finite state systems. The synthesis of infinite state systems, on the other hand, has only been investigated few times since then, with no complete or systematic solution. We present a systematic study of the synthesis of infinite state systems. The main step involves the synthesis of MSO-definable parity games, which is, finding MSO-definable uniform memoryless winning strategies for these games.

cs.LO↗
arXiv2024

Reinforcement Learning with LTL and $ω$-Regular Objectives via Optimality-Preserving Translation to Average Rewards

Linear temporal logic (LTL) and, more generally, $ω$-regular objectives are alternatives to the traditional discount sum and average reward objectives in reinforcement learning (RL), offering the advantage of greater comprehensibility and hence explainability. In this work, we study the relationship between these objectives. Our main result is that each RL problem for $ω$-regular objectives can be reduced to a limit-average reward problem in an optimality-preserving fashion, via (finite-memory) reward machines. Furthermore, we demonstrate the efficacy of this approach by showing that optimal policies for limit-average problems can be found asymptotically by solving a sequence of discount-sum problems approximately. Consequently, we resolve an open problem: optimal policies for LTL and $ω$-regular objectives can be learned asymptotically.

cs.LG↗
arXiv2024

Step length measurement in the wild using FMCW radar

With an aging population, numerous assistive and monitoring technologies are under development to enable older adults to age in place. To facilitate aging in place predicting risk factors such as falls, and hospitalization and providing early interventions are important. Much of the work on ambient monitoring for risk prediction has centered on gait speed analysis, utilizing privacy-preserving sensors like radar. Despite compelling evidence that monitoring step length, in addition to gait speed, is crucial for predicting risk, radar-based methods have not explored step length measurement in the home. Furthermore, laboratory experiments on step length measurement using radars are limited to proof of concept studies with few healthy subjects. To address this gap, a radar-based step length measurement system for the home is proposed based on detection and tracking using radar point cloud, followed by Doppler speed profiling of the torso to obtain step lengths in the home. The proposed method was evaluated in a clinical environment, involving 35 frail older adults, to establish its validity. Additionally, the method was assessed in people's homes, with 21 frail older adults who had participated in the clinical assessment. The proposed radar-based step length measurement method was compared to the gold standard Zeno Walkway Gait Analysis System, revealing a 4.5cm/8.3% error in a clinical setting. Furthermore, it exhibited excellent reliability (ICC(2,k)=0.91, 95% CI 0.82 to 0.96) in uncontrolled home settings. The method also proved accurate in uncontrolled home settings, as indicated by a strong agreement (ICC(3,k)=0.81 (95% CI 0.53 to 0.92)) between home measurements and in-clinic assessments.

cs.CV↗
arXiv2022

Effects of plasma on physical properties of water: nanocrystalline-to-amorphous phase transition and improving produce washing

Recently is was discovered in various applications that many physical and chemical properties of water change their temperature dependence between about 35 and 60 degrees Celsius. In particular, heat conductance, light absorption, and surface tension all change their temperature dependence. These drastic changes were associated with water gradually changing its mesoscopic structure: while at the higher temperatures water is a uniform media (amorphous state), at the temperatures below transition it consists of many nano-to-micro-scale clusters (crystalline state). This transition is similar to the second order phase transition. In the present paper we show that treating water with non-thermal plasma (adding plasma-created active compounds) can lower the temperature of the transition and thus cause a significant change in such physical quantities as surface tension, viscosity, freezing rate, and wettability and washability. We present analytical estimates of the transition temperature shift based on the Debya-Huckel theory. We discuss the produce-washing experiments that illustrate the predicted effects.

physics.plasm-ph↗
arXiv2021

Ambiguity Hierarchy of Regular Infinite Tree Languages

An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is k-ambiguous (for k > 0) if for every input it has at most k accepting computations. An automaton is boundedly ambiguous if it is k-ambiguous for some $k \in \mathbb{N}$. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. The degree of ambiguity of a regular language is defined in a natural way. A language is k-ambiguous (respectively, boundedly, finitely, countably ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly, finitely, countably ambiguous) automaton. Over finite words every regular language is accepted by a deterministic automaton. Over finite trees every regular language is accepted by an unambiguous automaton. Over $ω$-words every regular language is accepted by an unambiguous Büchi automaton and by a deterministic parity automaton. Over infinite trees Carayol et al. showed that there are ambiguous languages. We show that over infinite trees there is a hierarchy of degrees of ambiguity: For every k > 1 there are k-ambiguous languages that are not k - 1 ambiguous; and there are finitely (respectively countably, uncountably) ambiguous languages that are not boundedly (respectively finitely, countably) ambiguous.

cs.LO↗
arXiv2021

Some Complexity Results for Stateful Network Verification

In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour depends on a mutable internal state. Firewalls and load balancers are typical examples of stateful middleboxes. This work addresses the complexity of verifying safety properties, such as isolation, in networks with finite-state middleboxes. Unfortunately, we show that even in the absence of forwarding loops, reasoning about such networks is undecidable due to interactions between middleboxes connected by unbounded ordered channels. We therefore abstract away channel ordering. This abstraction is sound for safety, and makes the problem decidable. Specifically, safety checking becomes EXPSPACE-complete in the number of hosts and middleboxes in the network. To tackle the high complexity, we identify two useful subclasses of finite-state middleboxes which admit better complexities. The simplest class includes, e.g., firewalls and permits polynomial-time verification. The second class includes, e.g., cache servers and learning switches, and makes the safety problem coNP-complete. Finally, we implement a tool for verifying the correctness of stateful networks.

cs.LO↗
arXiv2018

A Proof of Stavi's Theorem

Kamp's theorem established the expressive equivalence of the temporal logic with Until and Since and the First-Order Monadic Logic of Order (FOMLO) over the Dedekind-complete time flows. However, this temporal logic is not expressively complete for FOMLO over the rationals. Stavi introduced two additional modalities and proved that the temporal logic with Until, Since and Stavi's modalities is expressively equivalent to FOMLO over all linear orders. We present a simple proof of Stavi's theorem.

cs.LO↗
arXiv2016

Methane Incorporation into Liquid Fuel by Non-Equilibrium Plasma Discharges

The conventional ways of processing natural gas into more efficient and economical fuels usually either have low conversion rate or low energy efficiency. In this work, a new approach of methane liquefaction is proposed. Instead of direct treatment of only natural gas, plasma activated methane is reacting with liquid fuel. In this way, methane molecules are directly incorporated onto liquid fuel to achieve liquefaction. Nanosecond-pulsed dielectric barrier discharge and atmospheric pressure glow discharge are used here to ensure no local heating in gas bubbles. Effects of both discharges on methane reaction with liquid fuel are investigated, mass and chemical changes in liquid are observed. Preliminary results show fixation of methane in liquid fuel.

physics.plasm-ph↗
arXiv2012

The Complexity of Multi-Mean-Payoff and Multi-Energy Games

In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of multi-energy games and show the inter-reducibility of multimean-payoff and multi-energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete. Finally we present the first solution of multi-meanpayoff games with infinite-memory strategies. We show that multi-mean-payoff games with mean-payoff-sup objectives can be decided in NP and coNP, whereas multi-mean-payoff games with mean-payoff-inf objectives are coNP-complete.

cs.GT↗
arXiv2011

Decidable Expansions of Labelled Linear Orderings

Consider a linear ordering equipped with a finite sequence of monadic predicates. If the ordering contains an interval of order type ωor -ω, and the monadic second-order theory of the combined structure is decidable, there exists a non-trivial expansion by a further monadic predicate that is still decidable.

cs.LO↗
arXiv2010

The complexity of linear-time temporal logic over the class of ordinals

We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem over the class of ordinals. Among the consequences of our proof, we show that given the code of some countable ordinal alpha and a formula, we can decide in PSPACE whether the formula has a model over alpha. In order to show these results, we introduce a class of simple ordinal automata, as expressive as Büchi ordinal automata. The PSPACE upper bound for the satisfiability problem of the temporal logic is obtained through a reduction to the nonemptiness problem for the simple ordinal automata.

cs.LO↗
arXiv2009

The Church Problem for Countable Ordinals

A fundamental theorem of Buchi and Landweber shows that the Church synthesis problem is computable. Buchi and Landweber reduced the Church Problem to problems about ω-games and used the determinacy of such games as one of the main tools to show its computability. We consider a natural generalization of the Church problem to countable ordinals and investigate games of arbitrary countable length. We prove that determinacy and decidability parts of the Bu}chi and Landweber theorem hold for all countable ordinals and that its full extension holds for all ordinals < ω\^ω.

cs.LO↗
arXiv2007

The Church Synthesis Problem with Parameters

For a two-variable formula &psi;(X,Y) of Monadic Logic of Order (MLO) the Church Synthesis Problem concerns the existence and construction of an operator Y=F(X) such that &psi;(X,F(X)) is universally valid over Nat. Büchi and Landweber proved that the Church synthesis problem is decidable; moreover, they showed that if there is an operator F that solves the Church Synthesis Problem, then it can also be solved by an operator defined by a finite state automaton or equivalently by an MLO formula. We investigate a parameterized version of the Church synthesis problem. In this version &psi; might contain as a parameter a unary predicate P. We show that the Church synthesis problem for P is computable if and only if the monadic theory of is decidable. We prove that the Büchi-Landweber theorem can be extended only to ultimately periodic parameters. However, the MLO-definability part of the Büchi-Landweber theorem holds for the parameterized version of the Church synthesis problem.

cs.LO↗
arXiv2007

A Logic of Reachable Patterns in Linked Data-Structures

We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The main feature of this logic is the ability to limit the neighborhood of a node that is reachable via a regular expression from a designated node. The logic is closed under boolean operations (entailment, negation) and has a finite model property. The key technical result is the proof of decidability. We show how to express precondition, postconditions, and loop invariants for some interesting programs. It is also possible to express properties such as disjointness of data-structures, and low-level heap mutations. Moreover, our logic can express properties of arbitrary data-structures and of an arbitrary number of pointer fields. The latter provides a way to naturally specify postconditions that relate the fields on entry to a procedure to the fields on exit. Therefore, it is possible to use the logic to automatically prove partial correctness of programs performing low-level heap mutations.

cs.LO↗
arXiv2007

Expressiveness of Metric modalities for continuous time

We prove a conjecture by A. Pnueli and strengthen it showing a sequence of "counting modalities" none of which is expressible in the temporal logic generated by the previous modalities, over the real line, or over the positive reals. Moreover, there is no finite temporal logic that can express all of them over the real line, so that no finite metric temporal logic is expressively complete.

cs.LO↗