arXiv subjects

Dylan Bellier

Publications and source records attributed to Dylan Bellier.

3 recordsLinked to original sources

arXiv2026

Interpreted Higher-Dimensional Automata for Concurrent Discrete-Event Control

In recent years the theory of Higher Dimensional Automata (HDA) has seen significant advances from a theoretical point of view, reflecting standard automata theory. There have also been first attempts to use the mathematical framework provided by HDAs to known problems, in particular Petri Net analysis. However real-world applications are still lacking and issues from real-world system, as concurrency, is still opened in the context of controller generation. In this work we show how the framework of HDAs can be adapted to help transforming controllers given as interpreted Petri nets (IPN) into an actual closed loop controller and how the HDA helps in identifying ambiguous or even contradictory specifications that remain hidden in the IPN. We demonstrate the feasibility by connecting the obtain controller to a virtual environment for closed loop control, exemplified by an industrial example.

cs.FL↗

arXiv2023

Alternating (In)Dependence-Friendly Logic

Hintikka and Sandu originally proposed Independence Friendly Logic (IF) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantics of natural language. The logic allows for expressing independence constraints among quantified variables, in a similar vein to Henkin quantifiers, and has a nice game-theoretic semantics in terms of imperfect information games. However, the IF semantics exhibits some limitations. It treats the players asymmetrically, considering only one of the two players as having imperfect information when evaluating truth, resp., falsity, of a sentence. In addition, the truth and falsity of sentences coincide with the existence of a uniform winning strategy for one of the two players in the semantic imperfect information game. As a consequence, IF does admit undetermined sentences, which are neither true nor false, thus failing the law of excluded middle. In this paper, we investigate an extension of IF, called Alternating Dependence/Independence Friendly Logic (ADIF), tailored to overcome these limitations. To this end, we introduce a novel compositional semantics, generalising the one based on trumps proposed by Hodges for IF. The new semantics (i) allows for meaningfully restricting both players at the same time, (ii) enjoys the property of game-theoretic determinacy, (iii) recovers the law of excluded middle for sentences, and (iv) grants ADIF the full descriptive power of Second Order Logic. We also provide an equivalent Herbrand-Skolem semantics and a game-theoretic semantics for the prenex fragment of ADIF, the latter being defined in terms of a determined infinite-duration game that precisely captures the other two semantics on finite structures.

cs.LO↗

arXiv2021

Good-for-Game QPTL: An Alternating Hodges Semantics

An extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the future values of the other variables. This restriction is tightly connected to the notion of behavioral strategies in game-theory and allows the resulting logic to naturally express game-theoretic concepts. The fragment where only restricted quantifications are considered, called behavioral quantifications, can be decided, for both model checking and satisfiability, in 2ExpTime and is expressively equivalent to QPTL, though significantly less succinct.

cs.LO↗