Episciences.org
Not a member yet
6707 research outputs found
Sort by
Automorphisms of -bundles over rational surfaces
No full textIn this paper we provide the complete classification of-bundles over smooth projective rational surfaces whose neutralcomponent of the automorphism group is maximal. Our results hold over anyalgebraically closed field of characteristic zero.Comment: 47 pages, final versio
Guarded Kleene Algebra with Tests: Automata Learning
No full textGuarded Kleene Algebra with Tests (GKAT) is the fragment of Kleene Algebrawith Tests (KAT) that arises by replacing the union and iteration operations ofKAT with predicate-guarded variants. GKAT is more efficiently decidable thanKAT and expressive enough to model simple imperative programs, making itattractive for applications to e.g. network verification. In this paper, wefurther explore GKAT's automata theory, and present GL*, an algorithm forlearning the GKAT automaton representation of a black-box, by observing itsbehaviour. A complexity analysis shows that it is more efficient to learn arepresentation of a GKAT program with GL* than with Angluin's existing L*algorithm. We implement GL* and L* in OCaml and compare their performances onexample programs
Bi-invariance for Uniform Strategies on Event Structures
No full textA recurring problem in game semantics is to enforce uniformity in strategies.Informally, a strategy is uniform when the Player's behaviour does not dependon the particular indexing of moves chosen by the Opponent. In game semantics,uniformity is used to define a resource modality !, that can be exploited forthe semantics of programming languages. In this paper we give a new account of uniformity for strategies on eventstructures. This work is inspired by an older idea due to Melli\`es, thatuniformity should be expressed as "bi-invariance" with respect to twointeracting group actions. We explore the algebraic foundations ofbi-invariance, adapt this idea to the language of event structures and define ageneral notion of uniform strategy in this context. Finally we revisit anexisting approach to uniformity, and show how this arises as a special case ofour constructions.Comment: Proceedings of MFPS 2022 (Final version
Further studies on open well-filtered spaces
No full textThe open well-filtered spaces were introduced by Shen, Xi, Xu and Zhao toanswer the problem whether every core-compact well-filtered space is sober. Inthe current paper we explore further properties of open well-filtered spaces.One of the main results is that if a space is open well-filtered, then so isits upper space (the set of all nonempty saturated compact subsets equippedwith the upper Vietoris topology). Some other properties on open well-filteredspaces are also studied
Proving exact values for the -limited broadcast domination number on grid graphs
No full textWe establish exact values for the -limited broadcast domination number ofvarious grid graphs, in particular for andall , for all , and for and all . We also produce periodically optimalvalues for and for , P_4 \squareP_n for , and for . Our method completesan exhaustive case analysis and eliminates cases by combining tools from linearprogramming with various mathematical proof techniques
Bounding conjugacy depth functions for wreath products of finitely generated abelian groups
No full textIn this article, we study the asymptotic behaviour of conjugacy separabilityfor wreath products of abelian groups. We fully characterise the asymptoticclass in the case of lamplighter groups and give exponential upper and lowerbounds for generalised lamplighter groups. In the case where the base group isinfinite, we give superexponential lower and upper bounds. We apply our resultsto obtain lower bounds for conjugacy depth functions of various wreath productsof groups where the acting group is not abelian.Comment: 33 pages. Published in journal of Groups, Complexity, Cryptology. arXiv admin note: substantial text overlap with arXiv:2111.1472
Error Correction for Discrete Tomography
No full textDiscrete tomography focuses on the reconstruction of functions from their line sums in a finite number of directions, where is a finite subset of . Consequently, the techniques ofdiscrete tomography often find application in areas where only a small numberof projections are available. In 1978 M.B. Katz gave a necessary and sufficientcondition for the uniqueness of the solution. Since then, severalreconstruction methods have been introduced. Recently Pagani and Tijdemandeveloped a fast method to reconstruct if it is uniquely determined.Subsequently Ceko, Pagani and Tijdeman extended the method to thereconstruction of a function with the same line sums of in the generalcase. Up to here we assumed that the line sums are exact. In this paper weinvestigate the case where a small number of line sums are incorrect as mayhappen when discrete tomography is applied for data storage or transmission. Weshow how less than errors can be corrected and that this bound is thebest possible.Comment: final versio
Reduction Free Normalisation for a proof irrelevant type of propositions
No full textWe show normalisation and decidability of convertibility for a type theorywith a hierarchy of universes and a proof irrelevant type of propositions,close to the type system used in the proof assistant Lean. Contrary to previousarguments, the proof does not require explicitly to introduce a notion ofneutral and normal forms
A framework to measure the robustness of programs in the unpredictable environment
No full textDue to the diffusion of IoT, modern software systems are often thought tocontrol and coordinate smart devices in order to manage assets and resources,and to guarantee efficient behaviours. For this class of systems, whichinteract extensively with humans and with their environment, it is thus crucialto guarantee their correct behaviour in order to avoid unexpected and possiblydangerous situations. In this paper we will present a framework that allows usto measure the robustness of systems. This is the ability of a program totolerate changes in the environmental conditions and preserving the originalbehaviour. In the proposed framework, the interaction of a program with itsenvironment is represented as a sequence of random variables describing howboth evolve in time. For this reason, the considered measures will be definedamong probability distributions of observed data. The proposed framework willbe then used to define the notions of adaptability and reliability. The formerindicates the ability of a program to absorb perturbation on environmentalconditions after a given amount of time. The latter expresses the ability of aprogram to maintain its intended behaviour (up-to some reasonable tolerance)despite the presence of perturbations in the environment. Moreover, analgorithm, based on statistical inference, is proposed to evaluate the proposedmetric and the aforementioned properties. We use two case studies to thedescribe and evaluate the proposed approach
A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
No full textMilner (1984) defined an operational semantics for regular expressions asfinite-state processes. In order to axiomatize bisimilarity of regularexpressions under this process semantics, he adapted Salomaa's proof systemthat is complete for equality of regular expressions under the languagesemantics. Apart from most equational axioms, Milner's system Mil inherits fromSalomaa's system a non-algebraic rule for solving single fixed-point equations.Recognizing distinctive properties of the process semantics that renderSalomaa's proof strategy inapplicable, Milner posed completeness of the systemMil as an open question. As a proof-theoretic approach to this problem we characterize thederivational power that the fixed-point rule adds to the purely equational partMil of Mil. We do so by means of a coinductive rule that permits cyclicderivations that consist of a finite process graph with empty steps thatsatisfies the layered loop existence and elimination property LLEE, and two ofits Mil-provable solutions. With this rule as replacement for thefixed-point rule in Mil, we define the coinductive reformulation cMil as anextension of Mil. In order to show that cMil and Mil are theoremequivalent we develop effective proof transformations from Mil to cMil, andvice versa. Since it is located half-way in between bisimulations and proofs inMilner's system Mil, cMil may become a beachhead for a completeness proof ofMil. This article extends our contribution to the CALCO 2022 proceedings. Here werefine the proof transformations by framing them as eliminations of derivableand admissible rules, and we link coinductive proofs to a coalgebraicformulation of solutions of process graphs.Comment: arXiv admin note: substantial text overlap with arXiv:2108.1310