arXiv subjects

Catalin Dima

Publications and source records attributed to Catalin Dima.

16 recordsLinked to original sources

arXiv2026

Weighing Timed Regular Languages: The Final Step (long version)

The bandwidth of a timed language characterizes the quantity of information per time unit (with a finite observation precision $\varepsilon$). The asymptotic behavior of the bandwidth as $\varepsilon \to 0$ classifies timed regular languages in three classes: meager, normal, and obese. Normal timed automata have a bounded frequency of events and some non-punctual transitions, and, up to now, were the only class of timed automata for which no algorithm was available for computing their bandwidth. In this article, we compute the bandwidth of any such automaton in the form $\approx\alpha\log{1/\varepsilon}$. Our approach reduces this problem to computing the best reward-to-cost ratio in a weighted finite graph constructed from the given timed automaton.

cs.FL↗

arXiv2025

Weighing Obese Timed Languages

The bandwidth of a timed language characterizes the quantity of information per time unit (with a finite observation precision $\varepsilon$). Obese timed automata have an unbounded frequency of events and produce information at the maximal possible rate. In this article, we compute the bandwidth of any such automaton in the form $\approx\alpha/\varepsilon$. Our approach reduces the problem to computing the best reward-to-time ratio in a weighted timed graph constructed from the given timed automaton, with weights corresponding to the entropy of auxiliary finite automata.

cs.FL↗

arXiv2024

Deciding the synthesis problem for hybrid games through bisimulation

Hybrid games are games played on a finite graph endowed with real variables which may model behaviors of discrete controllers of continuous systems. The synthesis problem for hybrid games is decidable for classical objectives (like LTL formulas) when the games are initialized singular, meaning that the slopes of the continuous variables are piecewise constant and variables are reset whenever their slope changes. The known proof adapts the region construction from timed games. In this paper we show that initialized singular games can be reduced, via a sequence of alternating bisimulations, to timed games, generalizing the known reductions by bisimulation from initialized singular automata to timed automata. Alternating bisimulation is the generalization of bisimulation to games, accomodating a strategy translation lemma by which, when two games are bisimilar and carry the same observations, each strategy in one of the games can be translated to a strategy in the second game such that all the outcomes of the second strategy satisfies the same property that are satisfied by the first strategy. The advantage of the proposed approach is that one may then use realizability tools for timed games to synthesize a winning strategy for a given objective, and then use the strategy translation lemma to obtain a winning strategy in the hybrid game for the same objective.

cs.LO↗

arXiv2024

Computing the Bandwidth of Meager Timed Automata

The bandwidth of timed automata characterizes the quantity of information produced/transmitted per time unit. We previously delimited 3 classes of TA according to the nature of their asymptotic bandwidth: meager, normal, and obese. In this paper, we propose a method, based on a finite-state simply-timed abstraction, to compute the actual value of the bandwidth of meager automata. The states of this abstraction correspond to barycenters of the faces of the simplices in the region automaton. Then the bandwidth is $\log 1/|z_0|$ where $z_0$ is the smallest root (in modulus) of the characteristic polynomial of this finite-state abstraction.

cs.FL↗

arXiv2024

Controller Synthesis in Timed B\"uchi Automata: Robustness and Punctual Guards

We consider the synthesis problem on timed automata with B\"uchi objectives, where delay choices made by a controller are subjected to small perturbations. Usually, the controller needs to avoid punctual guards, such as testing the equality of a clock to a constant. In this work, we generalize to a robustness setting that allows for punctual transitions in the automaton to be taken by controller with no perturbation. In order to characterize cycles that resist perturbations in our setting, we introduce a new structural requirement on the reachability relation along an accepting cycle of the automaton. This property is formulated on the region abstraction, and generalizes the existing characterization of winning cycles in the absence of punctual guards. We show that the problem remains within PSPACE despite the presence of punctual guards.

cs.GT↗

arXiv2023

Computationally Feasible Strategies

Real-life agents seldom have unlimited reasoning power. In this paper, we propose and study a new formal notion of computationally bounded strategic ability in multi-agent systems. The notion characterizes the ability of a set of agents to synthesize an executable strategy in the form of a Turing machine within a given complexity class, that ensures the satisfaction of a temporal objective in a parameterized game arena. We show that the new concept induces a proper hierarchy of strategic abilities -- in particular, polynomial-time abilities are strictly weaker than the exponential-time ones. We also propose an ``adaptive'' variant of computational ability which allows for different strategies for each parameter value, and show that the two notions do not coincide. Finally, we define and study the model-checking problem for computational strategies. We show that the problem is undecidable even for severely restricted inputs, and present our first steps towards decidable fragments.

cs.MA↗

arXiv2023

Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting Protocol

We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL$^*$ for both the {\em objective} and {\em subjective} variants of the state-based semantics with imperfect information, which are commonly used in the modeling and verification of multi-agent systems. Furthermore, we apply the theoretical result to the verification of coercion-resistance in the ThreeBallot voting system, a voting protocol that does not use cryptography. In particular, we show that natural simplifications of an initial model of the protocol are in fact bisimulations of the original model, and therefore satisfy the same ATL$^*$ properties, including coercion-resistance. These simplifications allow the model-checking tool MCMAS to terminate on models with a larger number of voters and candidates, compared with the initial model.

cs.MA↗

arXiv2023

Bandwidth of Timed Automata: 3 Classes

Timed languages contain sequences of discrete events ("letters'') separated by real-valued delays, they can be recognized by timed automata, and represent behaviors of various real-time systems. The notion of bandwidth of a timed language defined in a previous paper characterizes the amount of information per time unit, encoded in words of the language observed with some precision ε. In this paper, we identify three classes of timed automata according to the asymptotics of the bandwidth of their languages with respect to this precision ε: automata are either meager, with an O(1) bandwidth, normal, with a Θ(log (1/ε)) bandwidth, or obese, with Θ(1/ε) bandwidth. We define two structural criteria and prove that they partition timed automata into these three classes of bandwidth, implying that there are no intermediate asymptotic classes. The classification problem of a timed automaton is PSPACE-complete. Both criteria are formulated using morphisms from paths of the timed automaton to some finite monoids extending Puri's orbit graphs; the proofs are based on Simon's factorization forest theorem.

cs.FL↗

arXiv2022

Careful Autonomous Agents in Environments With Multiple Common Resources

Careful rational synthesis was defined in (Condurache et al. 2021) as a quantitative extension of Fisman et al.'s rational synthesis (Fisman et al. 2010), as a model of multi-agent systems in which agents are interacting in a graph arena in a turn-based fashion. There is one common resource, and each action may decrease or increase the resource. Each agent has a temporal qualitative objective and wants to maintain the value of the resource positive. One must find a Nash equilibrium. This problem is decidable. In more practical settings, the verification of the critical properties of multi-agent systems calls for models with many resources. Indeed, agents and robots consume and produce more than one type of resource: electric energy, fuel, raw material, manufactured goods, etc. We thus explore the problem of careful rational synthesis with several resources. We show that the problem is undecidable. We then propose a variant with bounded resources, motivated by the observation that in practical settings, the storage of resources is limited. We show that the problem becomes decidable, and is no harder than controller synthesis with Linear-time Temporal Logic objectives.

cs.LO↗

arXiv2022

Model Checking Strategic Abilities in Information-sharing Systems

We introduce a subclass of concurrent game structures (CGS) with imperfect information in which agents are endowed with private data-sharing capabilities. Importantly, our CGSs are such that it is still decidable to model-check these CGSs against a relevant fragment of ATL. These systems can be thought as a generalisation of architectures allowing information forks, in the sense that, in the initial states of the system, we allow information forks from agents outside a given set A to agents inside this A. For this reason, together with the fact that the communication in our models underpins a specialised form of broadcast, we call our formalism A-cast systems. To underline, the fragment of ATL for which we show the model-checking problem to be decidable over A-cast is a large and significant one; it expresses coalitions over agents in any subset of the set A. Indeed, as we show, our systems and this ATL fragments can encode security problems that are notoriously hard to express faithfully: terrorist-fraud attacks in identity schemes.

cs.LO↗

arXiv2020

A Hennessy-Milner Theorem for ATL with Imperfect Information

We show that a history-based variant of alternating bisimulation with imperfect information allows it to be related to a variant of Alternating-time Temporal Logic (ATL) with imperfect information by a full Hennessy-Milner theorem. The variant of ATL we consider has a common knowledge semantics, which requires that the uniform strategy available for a coalition to accomplish some goal must be common knowledge inside the coalition, while other semantic variants of ATL with imperfect information do not accommodate a Hennessy-Milner theorem. We also show that the existence of a history-based alternating bisimulation between two finite Concurrent Game Structures with imperfect information (iCGS) is undecidable.

cs.LO↗

arXiv2019

Model Checking ATL* on vCGS

We prove that the model checking ATL* on concurrent game structures with propositional control for atom-visibility (vCGS) is undecidable. To do so, we reduce this problem to model checking ATL* on iCGS.

cs.LO↗

arXiv2015

Entropy Games and Matrix Multiplication Games

Two intimately related new classes of games are introduced and studied: entropy games (EGs) and matrix multiplication games (MMGs). An EG is played on a finite arena by two-and-a-half players: Despot, Tribune and the non-deterministic People. Despot wants to make the set of possible People's behaviors as small as possible, while Tribune wants to make it as large as possible.An MMG is played by two players that alternately write matrices from some predefined finite sets. One wants to maximize the growth rate of the product, and the other to minimize it. We show that in general MMGs are undecidable in quite a strong sense.On the positive side, EGs correspond to a subclass of MMGs, and we prove that such MMGs and EGs are determined, and that the optimal strategies are simple. The complexity of solving such games is in NP\&coNP.

cs.GT↗

arXiv2014

Safraless Synthesis for Epistemic Temporal Specifications

In this paper we address the synthesis problem for specifications given in linear temporal single-agent epistemic logic, KLTL (or $KL_1$), over single-agent systems having imperfect information of the environment state. Van der Meyden and Vardi have shown that this problem is 2Exptime complete. However, their procedure relies on complex automata constructions that are notoriously resistant to efficient implementations as they use Safra-like determinization. We propose a "Safraless" synthesis procedure for a large fragment of KLTL. The construction transforms first the synthesis problem into the problem of checking emptiness for universal co-Büchi tree automata using an information-set construction. Then we build a safety game that can be solved using an antichain-based symbolic technique exploiting the structure of the underlying automata. The technique is implemented and applied to a couple of case studies.

cs.LO↗

arXiv2013

Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics

We identify a subproblem of the model-checking problem for the epistemic μ-calculus which is decidable. Formulas in the instances of this subproblem allow free variables within the scope of epistemic modalities in a restricted form that avoids embodying any form of common knowledge. Our subproblem subsumes known decidable fragments of epistemic CTL/LTL, may express winning strategies in two-player games with one player having imperfect information and non-observable objectives, and, with a suitable encoding, decidable instances of the model-checking problem for ATLiR.

cs.GT↗

arXiv2011

Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable

We propose a formal proof of the undecidability of the model checking problem for alternating- time temporal logic under imperfect information and perfect recall semantics. This problem was announced to be undecidable according to a personal communication on multi-player games with imperfect information, but no formal proof was ever published. Our proof is based on a direct reduction from the non-halting problem for Turing machines.

cs.LO↗