arXiv subjects

Rajab Aghamov

Publications and source records attributed to Rajab Aghamov.

6 recordsLinked to original sources

arXiv2026

On Modal Logics of Full Products of Neighborhood Frames

On the product of two neighborhood frames, three natural neighborhood functions can be defined: the horizontal one assigning to a point (x, y) the set of all supersets of the Cartesian product of U and y, where U is a neighborhood of x; the vertical analog; and the product neighborhood function assigning as neighborhoods all supersets of sets Cartesian products of U and V, for neighborhoods U of x and V of y. We define the tri-modal logics Tx+T and Dx+D of classes of full products equipped with all three neighborhood functions of neighborhood frames validating the logic T or D; thereby extending known product results for S4 and D4 to weaker systems. Two interaction principles arise: (sub) = []p -> [1]p & [2]p and (mix) = []p -> [1][2]p & [2][1]p, where the modality [] stands for the product neighborhood function and [1], [2] the horizontal and vertical ones. Namely, we show that Tx+T = T*T*T + (mix) and Dx+D = D*D*D + (mix), where * denotes fusion. Notably, (sub) and (mix) are equivalent over S4*S4*S4 and thus S4*S4*S4 + (mix) axiomatizes the logic of full products of topological spaces.

cs.LO↗

arXiv2025

Temporal Properties of Conditional Independence in Dynamic Bayesian Networks

Dynamic Bayesian networks (DBNs) are compact graphical representations used to model probabilistic systems where interdependent random variables and their distributions evolve over time. In this paper, we study the verification of the evolution of conditional-independence (CI) propositions against temporal logic specifications. To this end, we consider two specification formalisms over CI propositions: linear temporal logic (LTL), and non-deterministic Büchi automata (NBAs). This problem has two variants. Stochastic CI properties take the given concrete probability distributions into account, while structural CI properties are viewed purely in terms of the graphical structure of the DBN. We show that deciding if a stochastic CI proposition eventually holds is at least as hard as the Skolem problem for linear recurrence sequences, a long-standing open problem in number theory. On the other hand, we show that verifying the evolution of structural CI propositions against LTL and NBA specifications is in PSPACE, and is NP- and coNP-hard. We also identify natural restrictions on the graphical structure of DBNs that make the verification of structural CI properties tractable.

cs.AI↗

arXiv2025

Linear dynamical systems with continuous weight functions

In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems of how to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions as well as polynomial weight functions as a special case. Additionally, weight functions that are definable in an o-minimal extension of the theory of the reals with exponentiation, which can be shown to be piecewise continuous, are considered. In particular, good ergodic properties of o-minimal weight functions, instrumental to the computation of the mean payoff, are established. Besides general LDSs, the special cases of stochastic LDSs and LDSs with bounded orbits are addressed. Finally, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.

math.DS↗

arXiv2025

Model Checking Linear Temporal Logic with Standpoint Modalities

Standpoint linear temporal logic ($SLTL$) is a recently introduced extension of classical linear temporal logic ($LTL$) with standpoint modalities. Intuitively, these modalities allow to express that, from agent $a$'s standpoint, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities we introduce four new semantics, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to $SLTL$ under any of the five semantics. Furthermore we analyze the computational complexity of the corresponding model checking problems, obtaining PSPACE-completeness in three cases, which stands in contrast to the known EXPSPACE-completeness of the $SLTL$ satisfiability problem.

cs.LO↗

arXiv2024

Model Checking Markov Chains as Distribution Transformers

The conventional perspective on Markov chains considers decision problems concerning the probabilities of temporal properties being satisfied by traces of visited states. However, consider the following query made of a stochastic system modelling the weather: given the conditions today, will there be a day with less than 50\% chance of rain? The conventional perspective is ill-equipped to decide such problems regarding the evolution of the initial distribution. The alternate perspective we consider views Markov chains as distribution transformers: the focus is on the sequence of distributions on states at each step, where the evolution is driven by the underlying stochastic transition matrix. More precisely, given an initial distribution vector $μ$, a stochastic update transition matrix $M$, we ask whether the ensuing sequence of distributions $(μ, Mμ, M^2μ, \dots)$ satisfies a given temporal property. This is a special case of the model-checking problem for linear dynamical systems, which is not known to be decidable in full generality. The goal of this article is to delineate the classes of instances for which this problem can be solved, under the assumption that the dynamics is governed by stochastic matrices.

cs.LO↗

arXiv2019

Modal logic with the difference modality of topological $T_0$-spaces

The aim of the paper is to study the topological modal logic of $T_0$ spaces, with the difference modality (for $T_n$, where $n\geq1 $ the corresponding logics were known). We consider propositional modal logic with two modal operators $\square$ and $[\ne]$. $\square$ is interpreted as an interior operator and $[\ne]$ corresponds to the inequality relation. We introduce the logic $S4DT_0$ and show that $S4DT_0$ is the logic of all $T_0$ spaces and has the finite model property.

math.LO↗