arXiv subjects

Mishel Carelli

Publications and source records attributed to Mishel Carelli.

5 recordsLinked to original sources

arXiv2026

Disintegration Temporal Logic for Probabilistic Hyperproperties

We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-interference and perfect indistinguishability. DTL is based on the notion of measure disintegration from probability theory, which allows for conditioning probabilities on a finite or infinite sequence of events occurring during a program execution. This naturally supports reasoning about interacting stochastic systems, where complete executions of one component induce conditional probability distributions over another. We illustrate applications of DTL to systems interacting with stochastic environments, distributional properties of Markov decision processes, and probabilistic automata on infinite words, and discuss its relationship to existing probabilistic logics. While model checking Markov chains against full DTL is undecidable, we identify two decidable fragments that capture many hyperproperties of interest. The linear fragment admits a polynomial-time model-checking procedure based on linear-algebraic techniques and captures probabilistic information-flow properties such as perfect indistinguishability and history-based probabilistic non-interference. The qualitative fragment admits an automata-theoretic model-checking procedure that extends the standard algorithm for $\mathit{HyperCTL}^*$ with reasoning about bottom strongly connected components.

cs.LO↗

arXiv2026

Loop Termination and Generalized Collatz Sequences

Linear-constraint loops are programs whose transition relation is specified by a system of linear inequalities. The termination problem asks, given a loop, whether it admits an infinite computation. Decidability of termination remains open for linear-constraint loops over integers, rationals, and reals. We focus on loops over integers and show that they are tightly connected to generalized Collatz sequences - integer sequences generated by maps that are linear on each residue class modulo a fixed natural number. We prove that termination of one-variable linear-constraint loops is decidable in polynomial time, provided a long-standing conjecture about generalized Collatz sequences holds. Conversely, we show that any decision procedure for one-variable loops would prove or refute specific instances of this conjecture, which remain open. Moreover, we show that if a one-variable loop has a cyclic trace, then it also has a cyclic trace of length at most two.

cs.LO↗

arXiv2025

Closure and Complexity of Temporal Causality

Temporal causality defines what property causes some observed temporal behavior (the effect) in a given computation, based on a counterfactual analysis of similar computations. In this paper, we study its closure properties and the complexity of computing causes. For the former, we establish that safety, reachability, and recurrence properties are all closed under causal inference: If the effect is from one of these property classes, then the cause for this effect is from the same class. We also show that persistence and obligation properties are not closed in this way. These results rest on a topological characterization of causes which makes them applicable to a wide range of similarity relations between computations. Finally, our complexity analysis establishes improved upper bounds for computing causes for safety, reachability, and recurrence properties. We also present the first lower bounds for all of the classes.

cs.LO↗

arXiv2024

Transfinite version of the Mittag-Leffler condition for the vanishing of the derived limit

We give a necessary and sufficient condition for an inverse sequence $S_0 \leftarrow S_1 \leftarrow \dots$ indexed by natural numbers to have ${\rm lim}^1S=0$. This condition can be treated as a transfinite version of the Mittag-Leffler condition. We consider inverse sequences in an arbitrary abelian category having a generator and satisfying Grothendieck axioms ${\rm (AB3)}$ and ${\rm (AB4^*)}.$ We also show that the class of inverse sequences $S$ such that ${\rm lim}\: S={\rm lim}^1 S=0$ is the least class of inverse sequences containing the trivial inverse sequence and closed with respect to small limits and a certain type of extensions.

math.KT↗

arXiv2024

CTL* Verification and Synthesis using Existential Horn Clauses

This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^*$ specifications, based on translation to Existential Horn Clauses (EHCs). $CTL^*$ is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems. EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness. We develop the translation system \textit{Trans}, which given a verification problem consisting of a program $P$ and a specification $\phi$, builds a set of EHCs which is satisfiable iff $P$ satisfies $\phi$. We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given $CTL^*$ specification. We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for $CTL^*$ verification and synthesis.

cs.LO↗