Author: "Chennai Mathematical Institute [Inde]" - Searchworks@Jio Institute Digital Library Search Results

Your search keyword '"Chennai Mathematical Institute [Inde]"' showing total 52 results

Start Over Author "Chennai Mathematical Institute [Inde]"

52 results on '"Chennai Mathematical Institute [Inde]"'

1. Reversible Regular Languages: Logical and Algebraic Characterisations

Author: Amaldev Manuel, R. Govind, Paul Gastin, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Research Lab in Computer Science (ReLaX), Institute of Mathematical Sciences [Chennai] (IMSc)-Chennai Mathematical Institute [Inde]-Université de Bordeaux (UB)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), INDIAN INSTITUTE OF TECHNOLOGY GOA (IIT GOA), and Chennai Mathematical Institute [Inde]
Subjects: Algebra and Number Theory, automata, Computer science, Regular languages, semigroups, Theoretical Computer Science, Algebra, reversible languages, Computational Theory and Mathematics, Regular language, Logical conjunction, Computer Science::Logic in Computer Science, [INFO]Computer Science [cs], Algebraic number, first-order logic, Information Systems
Abstract: International audience; We present first-order (FO) and monadic second-order (MSO) logics with predicates 'between' and 'neighbour' that characterise the class of regular languages that are closed under the reverse operation and its subclasses. The ternary between predicate bet(x, y, z) is true if the position y is strictly between the positions x and z. The binary neighbour predicate N(x, y) is true when the the positions x and y are adjacent. It is shown that the class of reversible regular languages is precisely the class definable in the logics MSO(bet) and MSO(N). Moreover the class is definable by their existential fragments EMSO(bet) and EMSO(N), yielding a normal form for MSO formulas. In the first-order case, the logic FO(bet) corresponds precisely to the class of reversible languages definable in FO(
Published: 2021

2. Playing with repetitions in data words using energy games

Author: Figueira, Diego, Majumdar, Anirban, Praveen, M., Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Centre National de la Recherche Scientifique (CNRS), Research Lab in Computer Science (ReLaX), Institute of Mathematical Sciences [Chennai] (IMSc)-Chennai Mathematical Institute [Inde]-Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Chennai Mathematical Institute [Inde], ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017), and ANR-16-CE40-0007,DELTA,DÉfis pour la Logique, les Transducteurs et les Automates(2016)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science::Computer Science and Game Theory, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], 010102 general mathematics, ComputingMilieux_PERSONALCOMPUTING, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], F.1.1, F.3.1, 0102 computer and information sciences, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], 01 natural sciences, Logic in Computer Science (cs.LO), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, 0101 mathematics
Abstract: Logical Methods in Computer Science ; Volume 16, Issue 3 ; 1860-5974, We introduce two-player games which build words over infinite alphabets, and we study the problem of checking the existence of winning strategies. These games are played by two players, who take turns in choosing valuations for variables ranging over an infinite data domain, thus generating multi-attributed data words. The winner of the game is specified by formulas in the Logic of Repeating Values, which can reason about repetitions of data values in infinite data words. We prove that it is undecidable to check if one of the players has a winning strategy, even in very restrictive settings. However, we prove that if one of the players is restricted to choose valuations ranging over the Boolean domain, the games are effectively equivalent to single-sided games on vector addition systems with states (in which one of the players can change control states but cannot change counter values), known to be decidable and effectively equivalent to energy games. Previous works have shown that the satisfiability problem for various variants of the logic of repeating values is equivalent to the reachability and coverability problems in vector addition systems. Our results raise this connection to the level of games, augmenting further the associations between logics on data words and counter systems.
Published: 2020

3. Zone-based verification of timed automata: extrapolations, simulations and what next?

Author: Bouyer, Patricia, Gastin, Paul, Herbreteau, Frédéric, Sankur, Ocan, Srivathsan, B., Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), SUpervision of large MOdular and distributed systems (SUMO), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), and Chennai Mathematical Institute [Inde]
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Verification algorithms, [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], 68Q60, 03B70, D.2.4, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in Computer Science (cs.LO), F.1.1, [INFO]Computer Science [cs], Timed automata, Computer Science::Formal Languages and Automata Theory, ComputingMilieux_MISCELLANEOUS
Abstract: Timed automata have been introduced by Rajeev Alur and David Dill in the early 90's. In the last decades, timed automata have become the de facto model for the verification of real-time systems. Algorithms for timed automata are based on the traversal of their state-space using zones as a symbolic representation. Since the state-space is infinite, termination relies on finite abstractions that yield a finite representation of the reachable states. The first solution to get finite abstractions was based on extrapolations of zones, and has been implemented in the industry-strength tool Uppaal. A different approach based on simulations between zones has emerged in the last ten years, and has been implemented in the fully open source tool TChecker. The simulation-based approach has led to new efficient algorithms for reachability and liveness in timed automata, and has also been extended to richer models like weighted timed automata, and timed automata with diagonal constraints and updates. In this article, we survey the extrapolation and simulation techniques, and discuss some open challenges for the future., Invited contribution at FORMATS'22
Published: 2022

4. Reachability games with relaxed energy constraints

Author: Nicolas Markey, Loïc Hélouët, Ritam Raha, SUpervision of large MOdular and distributed systems (SUMO), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Department of Mathematics & Computer Science (Antwerp), University of Antwerp (UA), Chennai Mathematical Institute [Inde], Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), This work was supported by UMI Relax, Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Universiteit Antwerpen [Antwerpen], Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Universiteit Antwerpen = University of Antwerpen [Antwerpen], and Helouet, Loic
Subjects: FOS: Computer and information sciences, Computer Science::Computer Science and Game Theory, EXPTIME, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, co-NP, Upper and lower bounds, lcsh:QA75.5-76.95, Theoretical Computer Science, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Computer Science - Computer Science and Game Theory, Reachability, Games on graphs, 0502 economics and business, 0202 electrical engineering, electronic engineering, information engineering, 0101 mathematics, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], PSPACE, Mathematics, Computer. Automation, Discrete mathematics, Energy constraints, lcsh:Mathematics, 010102 general mathematics, 05 social sciences, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], lcsh:QA1-939, Computer Science Applications, Constraint (information theory), Computational Theory and Mathematics, 010201 computation theory & mathematics, Bounded function, Interval (graph theory), 020201 artificial intelligence & image processing, 050206 economic theory, lcsh:Electronic computers. Computer science, Computer Science and Game Theory (cs.GT), Information Systems
Abstract: We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i.e., for infinite runs). We then consider two kinds of relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, in the sense that it allows receiving more energy when the upper bound is already reached, but the extra energy will not be stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations. We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in co-NP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players., In Proceedings GandALF 2019, arXiv:1909.05979
Published: 2022

5. Séminaire de Probabilités LI

Author: Karandikar, R. L., Rao, B. V., Leuridan, Christophe, Vidmar, Matija, Miclo, Laurent, Patie, Pierre, Bernou, Armand, Caballero, Maria-Emilia, Rouault, Alain, Dedecker, Jérôme, Merlevède, Florence, Rio, Emmanuel, Brosset, Fabien, Klein, Thierry, Lagnoux, Agnès, Petit, Pierre, Marinelli, Carlo, Scarpa, Luca, Castaing, Charles, Marie, Nicolas, Fitte, Paul Raynaud De, Attal, Stéphane, Deschamps, Julien, Pellegrini, Clément, Eisenbaum, Nathalie, Chennai Mathematical Institute [Inde], Institut Fourier (IF), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), Department of Mathematics (University of Ljubljana), University of Ljubljana, Toulouse School of Economics (TSE-R), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-École des hautes études en sciences sociales (EHESS)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche pour l’Agriculture, l’Alimentation et l’Environnement (INRAE), School of Operations Research and Information Engineering (ORIE), Cornell University [New York], Laboratoire Jacques-Louis Lions (LJLL (UMR_7598)), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Instituto de Matematicas (UNAM), Universidad Nacional Autónoma de México = National Autonomous University of Mexico (UNAM), Laboratoire de Mathématiques de Versailles (LMV), Université de Versailles Saint-Quentin-en-Yvelines (UVSQ)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Mathématiques Appliquées Paris 5 (MAP5 - UMR 8145), Université Paris Descartes - Paris 5 (UPD5)-Institut National des Sciences Mathématiques et de leurs Interactions (INSMI)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Analyse et Mathématiques Appliquées (LAMA), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12)-Centre National de la Recherche Scientifique (CNRS)-Université Gustave Eiffel, Institut de Mathématiques de Toulouse UMR5219 (IMT), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale de l'Aviation Civile (ENAC), University College of London [London] (UCL), Faculty of Mathematics [Vienna], University of Vienna [Vienna], Université de Montpellier (UM), Modélisation aléatoire de Paris X (MODAL'X), Université Paris Nanterre (UPN), Laboratoire de Mathématiques Raphaël Salem (LMRS), Université de Rouen Normandie (UNIROUEN), Normandie Université (NU)-Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS), Institut Camille Jordan [Villeurbanne] (ICJ), École Centrale de Lyon (ECL), Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université Jean Monnet [Saint-Étienne] (UJM)-Centre National de la Recherche Scientifique (CNRS), Università degli studi di Genova = University of Genoa (UniGe), Institut National des Sciences Mathématiques et de leurs Interactions (INSMI)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Donati-Martin, Catherine, Lejay, Antoine, Rouault, Alain, Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-École des hautes études en sciences sociales (EHESS)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche pour l’Agriculture, l’Alimentation et l’Environnement (INRAE), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS), Institut Camille Jordan (ICJ), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université Jean Monnet - Saint-Étienne (UJM)-Centre National de la Recherche Scientifique (CNRS), Équations aux dérivées partielles, analyse (EDPA), and Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université Jean Monnet - Saint-Étienne (UJM)-Centre National de la Recherche Scientifique (CNRS)-École Centrale de Lyon (ECL)
Subjects: [MATH.MATH-PR]Mathematics [math]/Probability [math.PR], ComputingMilieux_MISCELLANEOUS
Abstract: International audience
Published: 2022

6. Diversity of solutions: An exploration through the lens of fixed-parameter tractability theory

Author: Michael R. Fellows, Frances A. Rosamond, Julien Baste, Mateus de Oliveira Oliveira, Lars Jaffke, Geevarghese Philip, Tomáš Masařík, Operational Research, Knowledge And Data (ORKAD), Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Universität Ulm - Ulm University [Ulm, Allemagne], University of Bergen (UiB), Warsaw University of Technology [Warsaw], Charles University [Prague] (CU), and Chennai Mathematical Institute [Inde]
Subjects: FOS: Computer and information sciences, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Linguistics and Language, Polynomial, Theoretical computer science, Discrete Mathematics (cs.DM), Computer science, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], 010103 numerical & computational mathematics, 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], 01 natural sciences, Language and Linguistics, Through-the-lens metering, Artificial Intelligence, Computer Science - Data Structures and Algorithms, 0202 electrical engineering, electronic engineering, information engineering, Point (geometry), Relevance (information retrieval), Data Structures and Algorithms (cs.DS), 05C85, 0101 mathematics, ComputingMilieux_MISCELLANEOUS, Variety (cybernetics), Dynamic programming, 010201 computation theory & mathematics, 020201 artificial intelligence & image processing, Computer Science - Discrete Mathematics, Diversity (business)
Abstract: When modeling an application of practical relevance as an instance of a combinatorial problem X, we are often interested not merely in finding one optimal solution for that instance, but in finding a sufficiently diverse collection of good solutions. In this work we initiate a systematic study of diversity from the point of view of fixed-parameter tractability theory. First, we consider an intuitive notion of diversity of a collection of solutions which suits a large variety of combinatorial problems of practical interest. We then present an algorithmic framework which --automatically-- converts a tree-decomposition-based dynamic programming algorithm for a given combinatorial problem X into a dynamic programming algorithm for the diverse version of X. Surprisingly, our algorithm has a polynomial dependence on the diversity parameter., Comment: Accepted to Twenty-Ninth International Joint Conference on Artificial Intelligence, {IJCAI} 2020, 16 pages
Published: 2022

7. Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages

Author: Adsul, Bharat, Gastin, Paul, Sarkar, Saptarshi, Weil, Pascal, Indian Institute of Technology Bombay (IIT Bombay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Research Lab in Computer Science (ReLaX), Institute of Mathematical Sciences [Chennai] (IMSc)-Chennai Mathematical Institute [Inde]-Université de Bordeaux (UB)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Bordelais de Recherche en Informatique (LaBRI), and Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Krohn Rhodes theorem, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Theory of computation → Concurrency, regular trace languages, propositional dynamic logic, Theory of computation → Algebraic language theory, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Theory of computation → Algebraic language theory phrases Mazurkiewicz traces, asynchronous automata, cascade product, Theory of computation → Modal and temporal logics, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Mazurkiewicz traces, 2012 ACM Subject Classification Theory of computation → Concurrency
Abstract: One of the main motivations for this work is to obtain a distributed Krohn-Rhodes theorem for Mazurkiewicz traces. Concretely, we focus on the recently introduced operation of local cascade product of asynchronous automata and ask if every regular trace language can be accepted by a local cascade product of "simple" asynchronous automata. Our approach crucially relies on the development of a local and past-oriented propositional dynamic logic (LocPastPDL) over traces which is shown to be expressively complete with respect to all regular trace languages. An event-formula of LocPastPDL allows to reason about the causal past of an event and a path-formula of LocPastPDL, localized at a process, allows to march along the sequence of past-events in which that process participates, checking for local regular patterns interspersed with local tests of other event-formulas. We also use additional constant formulas to compare the leading process events from the causal past. The new logic LocPastPDL is of independent interest, and the proof of its expressive completeness is rather subtle. Finally, we provide a translation of LocPastPDL formulas into local cascade products. More precisely, we show that every LocPastPDL formula can be computed by a restricted local cascade product of the gossip automaton and localized 2-state asynchronous reset automata and localized asynchronous permutation automata., LIPIcs, Vol. 243, 33rd International Conference on Concurrency Theory (CONCUR 2022), pages 28:1-28:19
Published: 2022
Full Text: View/download PDF

8. Asynchronous wreath product and cascade decompositions for concurrent behaviours

Author: Adsul, Bharat, Gastin, Paul, Sarkar, Saptarshi, Weil, Pascal, Indian Institute of Technology Bombay (IIT Bombay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Research Lab in Computer Science (ReLaX), Institute of Mathematical Sciences [Chennai] (IMSc)-Chennai Mathematical Institute [Inde]-Université de Bordeaux (UB)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Bordelais de Recherche en Informatique (LaBRI), and Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)
Subjects: FOS: Computer and information sciences, General Computer Science, Krohn Rhodes decomposition theorem, Formal Languages and Automata Theory (cs.FL), Computer Science - Formal Languages and Automata Theory, wreath product, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.3: Formal Languages/F.4.3.0: Algebraic language theory, Theoretical Computer Science, asynchronous automata, cascade product, local temporal logic over traces, [INFO]Computer Science [cs], Mazurkiewicz traces, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; We develop new algebraic tools to reason about concurrent behaviours modelled as languages of Mazurkiewicz traces and asynchronous automata. These tools reflect the distributed nature of traces and the underlying causality and concurrency between events, and can be said to support true concurrency. They generalize the tools that have been so efficient in understanding, classifying and reasoning about word languages. In particular, we introduce an asynchronous version of the wreath product operation and we describe the trace languages recognized by such products (the so-called asynchronous wreath product principle). We then propose a decomposition result for recognizable trace languages, analogous to the Krohn-Rhodes theorem, and we prove this decomposition result in the special case of acyclic architectures. Finally, we introduce and analyze two distributed automata-theoretic operations. One, the local cascade product, is a direct implementation of the asynchronous wreath product operation. The other, global cascade sequences, although conceptually and operationally similar to the local cascade product, translates to a more complex asynchronous implementation which uses the gossip automaton of Mukund and Sohoni. This leads to interesting applications to the characterization of trace languages definable in first-order logic: they are accepted by a restricted local cascade product of the gossip automaton and 2-state asynchronous reset automata, and also by a global cascade sequence of 2-state asynchronous reset automata. Over distributed alphabets for which the asynchronous Krohn-Rhodes theorem holds, a local cascade product of such automata is sufficient and this, in turn, leads to the identification of a simple temporal logic which is expressively complete for such alphabets.
Published: 2021
Full Text: View/download PDF

9. Remark on the global null controllability for a viscous Burgers-particle system with particle supported control

Author: Arnab Roy, Mythily Ramaswamy, Takéo Takahashi, Chennai Mathematical Institute [Inde], Institute of Mathematics of the Czech Academy of Science (IM / CAS), Czech Academy of Sciences [Prague] (CAS), Institut Élie Cartan de Lorraine (IECL), Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Systems with physical heterogeneities : inverse problems, numerical simulation, control and stabilization (SPHINX), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Arnab Roy and Takéo Takahashi were partially supported by the ANR research project IFSMACS (ANR-15-CE40-0010). The three authors were partially supported by the IFCAM project 'Analysis, Control and Homogenization of Complex Systems'., and ANR-15-CE40-0010,IFSMACS,Interaction Fluide-Structure : Modélisation, analyse, contrôle et simulation(2015)
Subjects: 0209 industrial biotechnology, Work (thermodynamics), Point particle, 02 engineering and technology, 01 natural sciences, Physics::Fluid Dynamics, Mathematics - Analysis of PDEs, 020901 industrial engineering & automation, Position (vector), Fluid-structure interaction, FOS: Mathematics, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], 0101 mathematics, Mathematics - Optimization and Control, Mathematics, Particle system, Applied Mathematics, 010102 general mathematics, Null (mathematics), Mathematical analysis, AMS subject classifications. 35Q35, 35D30, 35D35, 35R37, 35L10, 93D15, 93D20, global controllability, Burgers' equation, Controllability, viscous Burgers equation, Optimization and Control (math.OC), Particle, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Analysis of PDEs (math.AP)
Abstract: International audience; This paper is devoted to study the controllability of a one-dimensional fluid-particle interaction model where the fluid follows the viscous Burgers equation and the point mass obeys Newton's second law. We prove the null controllability for the velocity of the fluid and the particle and an approximate controllability for the position of the particle with a control variable acting only on the particle. One of the novelties of our work is the fact that we achieve this controllability result in a uniform time for all initial data and without any smallness assumptions on the initial data.
Published: 2020

10. Random presentations and random subgroups: a survey

Author: Bassino, Frédérique, Nicaud, Cyril, Weil, Pascal, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique Gaspard-Monge (LIGM), Centre National de la Recherche Scientifique (CNRS)-Fédération de Recherche Bézout-ESIEE Paris-École des Ponts ParisTech (ENPC)-Université Paris-Est Marne-la-Vallée (UPEM), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Research Lab in Computer Science - CNRS UMI 2000 (ReLaX), Frédérique Bassino, Ilya Kapovich, Markus Lohrey, Alexei Miasnikov, Cyril Nicaud, Andrey Nikolaev, Igor Rivin, Vladimir Shpilrain, Alexander Ushakov and Pascal Weil, ANR-16-CE40-0007,DELTA,DÉfis pour la Logique, les Transducteurs et les Automates(2016), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), Université Paris-Est Marne-la-Vallée (UPEM)-École des Ponts ParisTech (ENPC)-ESIEE Paris-Fédération de Recherche Bézout-Centre National de la Recherche Scientifique (CNRS), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), Research Lab in Computer Science (ReLaX), and Institute of Mathematical Sciences [Chennai] (IMSc)-Chennai Mathematical Institute [Inde]-Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)
Subjects: MSC 20F05, 20F10, 20E05, [MATH.MATH-GR]Mathematics [math]/Group Theory [math.GR]
Abstract: International audience; This is a survey of results on random group presentations, and on random subgroups of certain fixed groups. Being a survey, this paper does not contain new results, but it offers a synthetic view of a part of this very active field of research.
Published: 2020

11. A Bridge between Polynomial Optimization and Games with Imperfect Recall

Author: Gimbert, H., Paul, S., B Srivathsan, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], and Gimbert, Hugo
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science::Computer Science and Game Theory, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], ComputingMilieux_PERSONALCOMPUTING, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO] Computer Science [cs], Non-cooperative game theory, Logic in Computer Science (cs.LO), Computer Science - Computer Science and Game Theory, extensive form games, polynomial optimization, [INFO.INFO-GT] Computer Science [cs]/Computer Science and Game Theory [cs.GT], [INFO]Computer Science [cs], first order theory of reals, Bridge, complexity, Computer Science and Game Theory (cs.GT)
Abstract: International audience; We provide several positive and negative complexity results for solving games with imperfect recall. Using a one-to-one correspondence between these games on one side and multivariate polynomials on the other side, we show that solving games with imperfect recall is as hard as solving certain problems of the first order theory of reals. We establish square root sum hardness even for the specific class of A-loss games. On the positive side, we find restrictions on games and strategies motivated by Bridge bidding that give polynomial-time complexity.
Published: 2020

12. Why Liveness for Timed Automata Is Hard, and What We Can Do About It

Author: Igor Walukiewicz, B. Srivathsan, Thanh-Tung Tran, Frédéric Herbreteau, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), ANR-18-CE40-0015,TickTac,Techniques et outils efficaces pour la vérification et synthèse des systèmes temps-réels(2018), Chennai Mathematical Institute [Inde], and This work has been supported by project AVeRTS - CEFIPRA - Indo-French Program in ICST - DST/CNRS ref. 218093. Author B. Srivathsan is partially funded by a grant from Infosys Foundation.
Subjects: state subsumption, Property (philosophy), Theoretical computer science, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, General Computer Science, Logic, Reachability problem, Computer science, Liveness, Timed automaton, model-checking, liveness invariant, 0102 computer and information sciences, 02 engineering and technology, algorithms, 01 natural sciences, Theoretical Computer Science, Algorithmics, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Timed automata, 060201 languages & linguistics, 000 Computer science, knowledge, general works, liveness verification, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 06 humanities and the arts, Automaton, Computational Mathematics, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, 0602 languages and literature, Computer Science, Standard algorithms, 020201 artificial intelligence & image processing, State (computer science), complexity, Computer Science::Formal Languages and Automata Theory
Abstract: The reachability problem for timed automata asks if a given automaton has a run leading to an accepting state, and the liveness problem asks if the automaton has an infinite run that visits accepting states infinitely often. Both of these problems are known to be P space -complete. We show that if P ≠P space , the liveness problem is more difficult than the reachability problem; in other words, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is P space -hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it to existing solutions.
Published: 2020

13. Quadratically Tight Relations for Randomized Query Complexity

Author: Rahul Jain, Miklos Santha, Jevgēnijs Vihrovs, Srijita Kundu, Hartmut Klauck, Swagato Sanyal, Troy Lee, Ming Hsieh Department of Electrical Engineering [Los Angeles], USC Viterbi School of Engineering, University of Southern California (USC)-University of Southern California (USC), Chennai Mathematical Institute [Inde], Centre National de la Recherche Scientifique (CNRS), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Centre for Quantum Technologies [Singapore] (CQT), and National University of Singapore (NUS)
Subjects: Quadratic growth, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], 0209 industrial biotechnology, 0102 computer and information sciences, 02 engineering and technology, Measure (mathematics), Upper and lower bounds, 01 natural sciences, ACM: F.: Theory of Computation, Square (algebra), Computation Theory & Mathematics, Theoretical Computer Science, Combinatorics, Quadratic equation, 020901 industrial engineering & automation, Computational Theory and Mathematics, 010201 computation theory & mathematics, Theory of computation, Information complexity, [INFO]Computer Science [cs], 0102 Applied Mathematics, 0802 Computation Theory and Mathematics, 0805 Distributed Computing, Communication complexity, Boolean function, ComputingMilieux_MISCELLANEOUS, Mathematics
Abstract: In this work we investigate the problem of quadratically tightly approximating the randomized query complexity of Boolean functions R(f). The certificate complexity C(f) is such a complexity measure for the zero-error randomized query complexity R0(f): C(f) ≤R0(f) ≤C(f)2. In the first part of the paper we introduce a new complexity measure, expectational certificate complexity EC(f), which is also a quadratically tight bound on R0(f): EC(f) ≤R0(f) = O(EC(f)2). For R(f), we prove that EC2/3 ≤R(f). We then prove that EC(f) ≤C(f) ≤EC(f)2 and show that there is a quadratic separation between the two, thus EC(f) gives a tighter upper bound for R0(f). The measure is also related to the fractional certificate complexity FC(f) as follows: FC(f) ≤EC(f) = O(FC(f)3/2). This also connects to an open question by Aaronson whether FC(f) is a quadratically tight bound for R0(f), as EC(f) is in fact a relaxation of FC(f). In the second part of the work, we investigate whether the corruption bound corr𝜖(f) quadratically approximates R(f). By Yao’s theorem, it is enough to prove that the square of the corruption bound upper bounds the distributed query complexity $\mathsf {D}^{\mu }_{\epsilon }(f)$ for all input distributions μ. Here, we show that this statement holds for input distributions in which the various bits of the input are distributed independently. This is a natural and interesting subclass of distributions, and is also in the spirit of the input distributions studied in communication complexity in which the inputs to the two communicating parties are statistically independent. Our result also improves upon a result of Harsha et al. (2016), who proved a similar weaker statement. We also note that a similar statement in the communication complexity is open.
Published: 2020

14. On the Generalized Membership Problem in Relatively Hyperbolic Groups

Author: Pascal Weil, Olga Kharlampovich, Department of Mathematics and Statistics [Hunter College], Hunter College [CUNY, New York], City University of New York [New York] (CUNY)-City University of New York [New York] (CUNY), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Research Lab in Computer Science (ReLaX), Institute of Mathematical Sciences [Chennai] (IMSc)-Chennai Mathematical Institute [Inde]-Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Andreas Blass, Patrick Cégielski, Nachum Dershowitz, Manfred Droste, Bernd Finkbeiner, and ANR-16-CE40-0007,DELTA,DÉfis pour la Logique, les Transducteurs et les Automates(2016)
Subjects: Pure mathematics, Mathematics::Dynamical Systems, Membership problem, 010201 computation theory & mathematics, 010102 general mathematics, Structure (category theory), 0102 computer and information sciences, 0101 mathematics, 01 natural sciences, [MATH.MATH-GR]Mathematics [math]/Group Theory [math.GR], Mathematics, Decidability
Abstract: International audience; The aim of this short note is to provide a proof of the decidability of the generalized membership problem for relatively quasi-convex subgroups of finitely presented relatively hyperbolic groups, under some reasonably mild conditions on the peripheral structure of these groups. These hypotheses are satisfied, in particular, by toral relatively hyperbolic groups.
Published: 2020

15. On Functions Weakly Computable by Pushdown Petri Nets and Related Systems

Author: Leroux, Jérôme, Praveen, M., Schnoebelen, Philippe, Sutre, Grégoire, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université Sciences et Technologies - Bordeaux 1-Université Bordeaux Segalen - Bordeaux 2, Chennai Mathematical Institute [Inde], Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), and ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Formal Languages and Automata Theory (cs.FL), Pushdown vector addition systems, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Petri nets, Computer Science - Formal Languages and Automata Theory, Pumping lemma, 0102 computer and information sciences, 02 engineering and technology, Weak computation, 01 natural sciences, Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, Computer Science::Logic in Computer Science, Fast-growing functions, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], 020201 artificial intelligence & image processing, Computer Science::Formal Languages and Automata Theory, ComputingMilieux_MISCELLANEOUS
Abstract: We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growing functions $F_\alpha$ for $\alpha
Published: 2019
Full Text: View/download PDF

16. The Well Structured Problem for Presburger Counter Machines

Author: Finkel, Alain, Gupta, Ekanshdeep, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], Arkadev Chattopadhyay, Paul Gastin, and ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017)
Subjects: FOS: Computer and information sciences, 060201 languages & linguistics, Computer Science - Logic in Computer Science, 000 Computer science, knowledge, general works, Formal Languages and Automata Theory (cs.FL), Presburger counter machines, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science - Formal Languages and Automata Theory, 06 humanities and the arts, 02 engineering and technology, 16. Peace & justice, Condensed Matter::Mesoscopic Systems and Quantum Hall Effect, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Logic in Computer Science (cs.LO), Well structured transition systems, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 0602 languages and literature, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, infinite state systems, well structured problem, 020201 artificial intelligence & image processing, coverability, Computer Science::Formal Languages and Automata Theory, reachability
Abstract: We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS., Comment: version 2 of the FSTTCS'2019 paper
Published: 2019

17. Self-propelled motion of a rigid body inside a density dependent incompressible fluid

Author: Šárka Nečasová, Mythily Ramaswamy, Anja Schlömerkemper, Arnab Roy, Institute of Mathematics, Czech Academy of Sciences [Prague] (CAS), Chennai Mathematical Institute [Inde], Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Julius-Maximilians-Universität Würzburg [Wurtzbourg, Allemagne] (JMU), and Julius-Maximilians-Universität Würzburg (JMU)
Subjects: Angular momentum, Mathematics::Analysis of PDEs, Motion (geometry), Slip (materials science), Viscous liquid, 01 natural sciences, Physics::Fluid Dynamics, Mathematics - Analysis of PDEs, FOS: Mathematics, fluid-structure interaction system, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], 0101 mathematics, [MATH]Mathematics [math], Navier–Stokes equations, self-propelled motion, Physics, Applied Mathematics, Weak solution, 010102 general mathematics, Rigid body, nonnegative density, 010101 applied mathematics, Classical mechanics, Modeling and Simulation, Compressibility, Navier-Stokes equations, Analysis of PDEs (math.AP)
Abstract: This paper is devoted to the existence of a weak solution to a system describing a self-propelled motion of a rigid body in a viscous fluid in the whole ℝ3. The fluid is modelled by the incompressible nonhomogeneous Navier-Stokes system with a nonnegative density. The motion of the rigid body is described by the balance of linear and angular momentum. We consider the case where slip is allowed at the fluid-solid interface through Navier condition and prove the global existence of a weak solution.
Published: 2019

18. Verification of Flat FIFO Systems

Author: Finkel, Alain, Praveen, M., Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], and ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017)
Subjects: FOS: Computer and information sciences, termination, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Computer Science - Logic in Computer Science, ACM: F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES/F.1.1: Models of Computation, counters, flat systems, ACM: F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES, [SCCO.COMP]Cognitive science/Computer science, 0102 computer and information sciences, 02 engineering and technology, Computational Complexity (cs.CC), 01 natural sciences, 0202 electrical engineering, electronic engineering, information engineering, Infinite state systems, 000 Computer science, knowledge, general works, FIFO, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs, Logic in Computer Science (cs.LO), Computer Science - Computational Complexity, Theory of computation - Parallel computing models, 010201 computation theory & mathematics, Computer Science, 020201 artificial intelligence & image processing, complexity, reachability
Abstract: Logical Methods in Computer Science ; Volume 16, Issue 4 ; 1860-5974, The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO machines, generalizing similar existing results for flat counter machines. We also show that reachability is NP-complete for flat lossy FIFO machines and for flat front-lossy FIFO machines. We construct a trace-flattable system of many counter machines communicating via rendez-vous that is bisimilar to a given flat FIFO machine, which allows to model-check the original flat FIFO machine. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO machines based on analysis of flat sub-machines.
Published: 2019

19. SUR DEUX PROBLEMES DE HARDY ET MAHLER

Author: Philippon, Patrice, Rath, Purusottam, Institut de Mathématiques de Jussieu - Paris Rive Gauche (IMJ-PRG (UMR_7586)), Université Paris Diderot - Paris 7 (UPD7)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), and Chennai Mathematical Institute [Inde]
Subjects: [MATH.MATH-NT]Mathematics [math]/Number Theory [math.NT]
Abstract: It is a classical result of Mahler that for any rational number α > 1 which is not an integer and any real 0 < c < 1, the set of positive integers n such that α n < c n is necessarily finite. Here for any real x, x denotes the distance from its nearest integer. The problem of classifying all real algebraic numbers greater than one exhibiting the above phenomenon was suggested by Mahler. This was solved by a beautiful work of Corvaja and Zannier. On the other hand, for non-zero real numbers λ and α with α > 1, Hardy about a century ago asked "In what circumstances can it be true that λα n → 0 as n → ∞? " This question is still open in general. In this note, we study its analogue in the context of the problem of Mahler. We first compare and contrast with what is known visa -vis the original question of Hardy. We then suggest a number of questions that arise as natural consequences of our investigation. Of these questions, we answer one and offer some insight into others.
Published: 2019

20. Revisiting local time semantics for networks of timed automata

Author: Govind, R, Herbreteau, Frédéric, Srivathsan, B., Walukiewicz, Igor, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Chennai Mathematical Institute [Inde], and Srivathsan, B
Subjects: FOS: Computer and information sciences, State-space explosion due to interleavings, Computer Science - Logic in Computer Science, 68Q60, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], 000 Computer science, knowledge, general works, Formal Languages and Automata Theory (cs.FL), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science - Formal Languages and Automata Theory, Reachability, [INFO] Computer Science [cs], Logic in Computer Science (cs.LO), Computer Science, [INFO]Computer Science [cs], Astrophysics::Earth and Planetary Astrophysics, Timed automata, Zones and abstractions, Local-time semantics
Abstract: We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion is particularly visible as even different interleavings of local actions of processes may lead to different zones. Salah et al. in 2006 have shown that the union of all these different zones is also a zone. This observation was used in an algorithm which from time to time detects and aggregates these zones into a single zone. We show that such aggregated zones can be calculated more efficiently using the local time semantics and the related notion of local zones proposed by Bengtsson et al. in 1998. Next, we point out a flaw in the existing method to ensure termination of the local zone graph computation. We fix this with a new algorithm that builds the local zone graph and uses abstraction techniques over (standard) zones for termination. We evaluate our algorithm on standard examples. On various examples, we observe an order of magnitude decrease in the search space. On the other examples, the algorithm performs like the standard zone algorithm., Comment: A shorter version appears in proceedings of CONCUR 2019
Published: 2019
Full Text: View/download PDF

21. FPT Algorithms for Diverse Collections of Hitting Sets

Author: Julien Baste, Geevarghese Philip, Günter Rote, Tomáš Masařík, Lars Jaffke, Universität Ulm - Ulm University [Ulm, Allemagne], University of Bergen (UiB), Department of Applied Mathematics and Institute of Theoretical Computer Science (Charles University), Charles University [Prague] (CU), Warsaw University of Technology [Warsaw], Chennai Mathematical Institute [Inde], Department of Mathematics and Computer Science (Freie Universität Berlin), and Freie Universität Berlin
Subjects: FOS: Computer and information sciences, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Discrete Mathematics (cs.DM), Computer science, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], Parameterized complexity, 02 engineering and technology, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], Knotenabdeckungsproblem, Theoretical Computer Science, Set (abstract data type), Unterschiede, Vertex cover, Hamming distance, Computer Science - Data Structures and Algorithms, Parameter estimation, 0202 electrical engineering, electronic engineering, information engineering, Parameter (Mathematik), Hamming-Abstand, Data Structures and Algorithms (cs.DS), Solution diversity, 000 Informatik, Informationswissenschaft, allgemeine Werke::000 Informatik, Wissen, Systeme::004 Datenverarbeitung, Informatik, DDC 000 / Computer science, information & general works, DDC 004 / Data processing & computer science, Diversity Management, Feedback-vertex-set-Problem, Hitting sets, Feedback vertex set, Numerical Analysis, Algorithms in computation and mathematics, 020206 networking & telecommunications, Flow network, Computational Mathematics, Computational Theory and Mathematics, Fixed-parameter tractability, ddc:000, 020201 artificial intelligence & image processing, Pairwise comparison, ddc:004, Computational problem, Hamming code, Algorithm, Computer Science - Discrete Mathematics
Abstract: In this work, we study the $d$-Hitting Set and Feedback Vertex Set problems through the paradigm of finding diverse collections of $r$ solutions of size at most $k$ each, which has recently been introduced to the field of parameterized complexity [Baste et al., 2019]. This paradigm is aimed at addressing the loss of important side information which typically occurs during the abstraction process which models real-world problems as computational problems. We use two measures for the diversity of such a collection: the sum of all pairwise Hamming distances, and the minimum pairwise Hamming distance. We show that both problems are FPT in $k + r$ for both diversity measures. A key ingredient in our algorithms is a (problem independent) network flow formulation that, given a set of `base' solutions, computes a maximally diverse collection of solutions. We believe that this could be of independent interest., 17 pages, 3 figures
Published: 2019

22. Regular Transducer Expressions for Regular Transformations

Author: Vrunda Dave, Shankara Narayanan Krishna, Paul Gastin, Indian Institute of Technology Bombay (IIT Bombay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Research Lab in Computer Science (ReLaX), and Institute of Mathematical Sciences [Chennai] (IMSc)-Chennai Mathematical Institute [Inde]-Université de Bordeaux (UB)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)
Subjects: FOS: Computer and information sciences, Monoid, Pure mathematics, Formal Languages and Automata Theory (cs.FL), Transducers, Büchi automaton, Computer Science - Formal Languages and Automata Theory, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Theoretical Computer Science, symbols.namesake, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Regular expression, Unambiguity, Mathematics, Discrete mathematics, String (computer science), Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing), Regular expressions, Transition monoid, Expression (mathematics), Computer Science Applications, Cauchy product, Computational Theory and Mathematics, 010201 computation theory & mathematics, Weierstrass factorization theorem, symbols, 020201 artificial intelligence & image processing, Constant function, Computer Science::Formal Languages and Automata Theory, Information Systems
Abstract: International audience; Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, captured by a deterministic two-way transducer, can be described with a regular transducer expression (RTE). For infinite words, the two-way transducer uses Muller acceptance and ω-regular look-ahead. RTEs are constructed from constant functions using the combinators if-then-else (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product, the 2-chained Kleene-iteration and the 2-chained omega-iteration. Our proof works for transformations of both finite and infinite words, extending the result on finite words of Alur et al. in LICS'14. The construction of an RTE associated with a deterministic two-way transducer is guided by a regular expression which is "good" wrt. its transition monoid. "Good" expressions are unambiguous, ensuring the functionality of the output computed. Moreover, in "good" expressions, iterations (Kleene-plus or omega) are restricted to subexpressions corresponding to idempotent elements of the transition monoid. "Good" expressions can be obtained with an unambiguous version of Imre Simon's famous forest factorization theorem. To handle infinite words, we introduce the notion of transition monoids for deterministic two-way Muller transducers with look-ahead, where the look-ahead is captured by some backward deterministic Büchi automaton. This paper is an extended version of [15] presented at LICS'18.
Published: 2018

23. Playing with Repetitions in Data Words Using Energy Games

Author: Diego Figueira, M. Praveen, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], Research Lab in Computer Science - CNRS UMI 2000 (ReLaX), and ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017)
Subjects: Computer Science::Computer Science and Game Theory, Theoretical computer science, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Computer science, Data domain, ComputingMilieux_PERSONALCOMPUTING, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], 01 natural sciences, Undecidable problem, Connection (mathematics), Decidability, Boolean domain, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, Reachability, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Boolean satisfiability problem, Change control
Abstract: International audience; We introduce two-player games which build words over infinite alphabets, and we study the problem of checking the existence of winning strategies. These games are played by two players, who take turns in choosing valuations for variables ranging over an infinite data domain, thus generating multi-attributed data words. The winner of the game is specified by formulas in the Logic of Repeating Values, which can reason about repetitions of data values in infinite data words. We prove that it is undecidable to check if one of the players has a winning strategy, even in very restrictive settings. However, we prove that if one of the players is restricted to choose valuations ranging over the Boolean domain, the games are effectively equivalent to single-sided games on vector addition systems with states (in which one of the players can change control states but cannot change counter values), known to be decidable and effectively equivalent to energy games. Previous works have shown that the satisfiability problem for various variants of the logic of repeating values is equivalent to the reachability and coverability problems in vector addition systems. Our results raise this connection to the level of games, augmenting further the associations between logics on data words and counter systems.
Published: 2018

24. Width of Non-deterministic Automata

Author: Kuperberg, Denis, Majumdar, Anirban, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Preuves et Langages (PLUME), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], Palse Impulsion, École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), and Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL)
Subjects: 060201 languages & linguistics, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, 000 Computer science, knowledge, general works, non-deterministic automata, good-for-games, F43 Formal Languages Keywords and phrases width, 06 humanities and the arts, 02 engineering and technology, Nonlinear Sciences::Cellular Automata and Lattice Gases, 1998 ACM Subject Classification F11 Models of computations, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, determinisation, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 0602 languages and literature, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, complexity, Computer Science::Databases, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; We introduce a measure called width, quantifying the amount of nondeterminism in automata. Width generalises the notion of good-for-games (GFG) automata, that correspond to NFAs of width 1, and where an accepting run can be built on-the-fly on any accepted input. We describe an incremental determinisation construction on NFAs, which can be more efficient than the full powerset determinisation, depending on the width of the input NFA. This construction can be generalised to infinite words, and is particularly well-suited to coBüchi automata in this context. For coBüchi automata, this procedure can be used to compute either a deterministic automaton or a GFG one, and it is algorithmically more efficient in this last case. We show this fact by proving that checking whether a coBüchi automaton is determinisable by pruning is NP-complete. On finite or infinite words, we show that computing the width of an automaton is PSPACE-hard. 1 Introduction Determinisation of non-deterministic automata (NFAs) is one of the cornerstone problems of automata theory, with countless applications in verification. There is a very active field of research for optimizing or approximating determinisation, or circumventing it in contexts like inclusion of NFA or Church Synthesis. Indeed, determinisation is a costly operation, as the state space blow-up is in O(2 n) on finite words, O(3 n) for coBüchi automata [16], and 2 O(n log(n)) for Büchi automata [17]. If A and B are NFAs, the classical way of checking the inclusion L(A) ⊆ L(B) is to determinise B, complement it, and test emptiness of L(A) ∩ L(B). To circumvent a full determinisation, the recent algorithm from [3] proved to be very efficient, as it is likely to explore only a part of the powerset construction. Other approaches use simulation games to approximate inclusion at a cheaper cost, see for instance [8]. Another approach consists in replacing determinism by a weaker constraint that suffices in some particular context. In this spirit, Good-for-Games automata (GFG for short) were introduced in [9], as a way to solve the Church synthesis problem. This problem asks, given a specification L, typically given by an LTL formula, over an alphabet of inputs and outputs, whether there is a reactive system (transducer) whose behaviour is included in L. The classical solution computes a deterministic automaton for L, and solves a game defined on this automaton. It turns out that replacing determinism by the weaker constraint of being GFG is sufficient in this context. Intuitively, GFG automata are non-deterministic * This work was supported by the grant PALSE Impulsion.
Published: 2018

25. Parameterized Verification of Synchronization in Constrained Reconfigurable Broadcast Networks

Author: Nathalie Bertrand, Nicolas Markey, A. R. Balasubramanian, Chennai Mathematical Institute [Inde], SUpervision of large MOdular and distributed systems (SUMO), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Theoretical computer science, Formal Languages and Automata Theory (cs.FL), Computer science, Parameterized complexity, Computer Science - Formal Languages and Automata Theory, 02 engineering and technology, Broadcasting, 03 medical and health sciences, 0302 clinical medicine, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 0202 electrical engineering, electronic engineering, information engineering, Time complexity, [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], business.industry, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 16. Peace & justice, Logic in Computer Science (cs.LO), Undecidable problem, Decidability, Formalism (philosophy of mathematics), Computer Science - Distributed, Parallel, and Cluster Computing, [INFO.INFO-MA]Computer Science [cs]/Multiagent Systems [cs.MA], 030220 oncology & carcinogenesis, 020201 artificial intelligence & image processing, Distributed, Parallel, and Cluster Computing (cs.DC), business
Abstract: Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial communication topology). We focus here on the synchronization property, asking whether all agents converge to a set of target states after some execution. This problem is known to be decidable in polynomial time when no constraints are imposed on the evolution of the communication topology (while it is undecidable for static broadcast networks). In this paper we investigate how various constraints on reconfigurations affect the decidability and complexity of the synchronization problem. In particular, we show that when bounding the number of reconfigured links between two communications steps by a constant, synchronization becomes undecidable; on the other hand, synchronization remains decidable in PTIME when the bound grows with the number of agents., Accepted for publication in TACAS 2018
Published: 2018

26. Checking conformance for time-constrained scenario-based specifications

Author: Sundararaman Akshay, Paul Gastin, Madhavan Mukund, K. Narayan Kumar, Department of Computer Science and Engineering [Bombay], Indian Institute of Technology Bombay (IIT Bombay), Modeling and Exploitation of Interaction and Concurrency (MEXICO), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), and Chennai Mathematical Institute [Inde]
Subjects: Model checking, Finite-state machine, Theoretical computer science, General Computer Science, Computer science, Timed automaton, Abstraction model checking, Automata, Model Checking, Theoretical Computer Science, Undecidable problem, System model, Automaton, Message Sequence Charts, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Regular language, Msc Graphs, Timed Automata, Petri Nets, Unfoldings, ComputingMilieux_MISCELLANEOUS
Abstract: We consider the problem of model checking message-passing systems with real-time requirements. As behavioral specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behavior can be regarded as a timed automaton. Our goal is to verify that all timed behaviors exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking/conformance problem. (C) 2015 Elsevier B.V. All rights reserved.
Published: 2015

27. Controlling a Population

Author: Bertrand, Nathalie, Dewaskar, Miheer, Genest, Blaise, Gimbert, Hugo, Institut de Radioprotection et de Sûreté Nucléaire (IRSN), Chennai Mathematical Institute [Inde], SUpervision of large MOdular and distributed systems (SUMO), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), University of North Carolina [Chapel Hill] (UNC), University of North Carolina System (UNC), and ANR-13-BS02-0011,Stoch-MC,Modèles stochastiques: passage à l'échelle pour le Model Checking(2013)
Subjects: FOS: Computer and information sciences, Computer Science::Computer Science and Game Theory, 000 Computer science, knowledge, general works, [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], Formal Languages and Automata Theory (cs.FL), [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Computer Science - Formal Languages and Automata Theory, Systems and Control (eess.SY), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Computer Science - Computer Science and Game Theory, Computer Science, FOS: Electrical engineering, electronic engineering, information engineering, Computer Science - Systems and Control, Computer Science and Game Theory (cs.GT)
Abstract: International audience; We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such populations: no matter how individual agents react to the actions of the controller , the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a non-deterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2-player game. The first player (Controller) chooses actions, and the second player (Agents) resolves non-determinism for each agent. The game with m agents is called the m-population game. This gives rise to a parameterized control problem (where control refers to 2 player games), namely the population control problem: can Controller control the m-population game for all m ∈ N whatever Agents does? In this paper, we prove that the population control problem is decidable, and it is a EXPTIME-complete problem. As far as we know, this is one of the first results on parameterized control. Our algorithm, not based on cutoff techniques, produces winning strategies which are symbolic, that is, they do not need to count precisely how the population is spread between states. We also show that if there is no winning strategy, then there is a population size M such that Controller wins the m-population game if and only if m $≤ M$ . Surprisingly, M can be doubly exponential in the number of states of the NFA, with tight upper and lower bounds.
Published: 2017

28. A multitype Hawk and Dove game

Author: Aradhye, Aditya, Altman, Eitan, El-Azouzi, Rachid, Chennai Mathematical Institute [Inde], Network Engineering and Operations (NEO ), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA), Laboratory of Information, Network and Communication Sciences (LINCS), Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut Mines-Télécom [Paris] (IMT), Avignon Université (AU), Institut Mines-Télécom [Paris] (IMT)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC), and Altman, Eitan
Subjects: [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], [INFO.INFO-GT] Computer Science [cs]/Computer Science and Game Theory [cs.GT]
Abstract: International audience; We consider in this paper the Hawk-Dove game in which each of infinitely many individuals, involved with pairwise encounters with other individuals, can decide whether to act aggressively (Hawk) or peacefully (Dove). Each individual is characterized by its strength. The strength distribution among the population is assumed to be fixed and not to vary in time. If both individuals involved in an interaction are Hawks, there will be a fight, the result of which will be determined by the strength of each of the individuals involved. The larger the difference between the strength of the individuals is, the larger is the cost for the weaker player involved in the fight. Our goal is to study the influence of the parameters (such as the strength level distribution) on the equilibrium of the game. We show that for some parameters there exists a threshold equilibrium policy while for other parameters there is no equilibrium policy at all.
Published: 2017

29. On the Spectral Properties of Symmetric Functions

Author: Ada, Anil, Fawzi, Omar, Kulkarni, Raghav, Carnegie Mellon University [Pittsburgh] (CMU), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), and École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Subjects: FOS: Computer and information sciences, Mathematics - Functional Analysis, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Computer Science - Computational Complexity, Mathematics::Commutative Algebra, FOS: Mathematics, Computational Complexity (cs.CC), [MATH.MATH-FA]Mathematics [math]/Functional Analysis [math.FA], Functional Analysis (math.FA)
Abstract: We characterize the approximate monomial complexity, sign monomial complexity , and the approximate L 1 norm of symmetric functions in terms of simple combinatorial measures of the functions. Our characterization of the approximate L 1 norm solves the main conjecture in [AFH12]. As an application of the characterization of the sign monomial complexity, we prove a conjecture in [ZS09] and provide a characterization for the unbounded-error communication complexity of symmetric-xor functions.
Published: 2017

30. Contextual Array Grammars with Matrix and Regular Control

Author: Rani Siromoney, Rudolf Freund, K. G. Subramanian, Henning Fernau, Universität Trier, Vienna University of Technology (TU Wien), Chennai Mathematical Institute [Inde], Liverpool Hope University, Cezar Câmpeanu, Florin Manea, Jeffrey Shallit, TC 1, and WG 1.2
Subjects: business.industry, Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing), 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Matrix (mathematics), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Rule-based machine translation, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], 020201 artificial intelligence & image processing, Artificial intelligence, Alphabet, Arithmetic, Control (linguistics), business, computer, Computer Science::Formal Languages and Automata Theory, Natural language processing, Mathematics
Abstract: International audience; We investigate the computational power of d-dimensional contextual array grammars with matrix control and regular control languages. For $$d\ge 2$$, d-dimensional contextual array grammars are less powerful than matrix contextual array grammars, which themselves are less powerful than contextual array grammars with regular control languages. Yet in the 1-dimensional case, for a one-letter alphabet, the family of 1-dimensional array languages generated by contextual array grammars with regular control languages coincides with the family of regular 1-dimensional array languages, whereas for alphabets with more than one letter, we obtain the array images of the linear languages.
Published: 2016

31. ON COMPLETE REDUCIBILITY IN CHARACTERISTIC p

Author: Vikraman Balaji, Deligne, P., Parameswaran, A. J., Yun, Z., Balaji, Vikraman, Chennai Mathematical Institute [Inde], Institute for Advanced Study, Princeton University, Héritages et Constructions dans le Texte et l'Image (HCTI), Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Institut Brestois des Sciences de l'Homme et de la Société (IBSHS), Université de Brest (UBO)-Université de Brest (UBO), Tata Institue of Fundamental research, Department of Mathematics [Stanford], Stanford University, Institut Brestois des Sciences de l'Homme et de la Société (IBSHS), and Université de Brest (UBO)-Université de Brest (UBO)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)
Subjects: Algebraic Groups, complete reducibility, MSC-class:14L15, 14L24, etale slice, [MATH] Mathematics [math], [MATH]Mathematics [math]
Abstract: Let $G$ be a reductive group over a field $k$ which is algebraically closedof characteristic $p \neq 0$. We prove a structure theorem for a class ofsubgroup schemes of $G$, for $p$ bounded below by the Coxeter number of $G$. Asapplications, we derive semi-simplicity results, generalizing earlier resultsof Serre proven in 1998, and also obtain an analogue of Luna's \'etale slicetheorem for suitable bounds on $p$.
Published: 2016

32. The Higson-Roe exact sequence and $\ell^2$ eta invariants

Author: Benameur, Moulay-Tahar, Roy, Indrava, Institut Montpelliérain Alexander Grothendieck (IMAG), Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS), and Chennai Mathematical Institute [Inde]
Subjects: 58J28, 19K56, 58J32, [MATH.MATH-GT]Mathematics [math]/Geometric Topology [math.GT], Mathematics - K-Theory and Homology, [MATH.MATH-OA]Mathematics [math]/Operator Algebras [math.OA], Mathematics - Operator Algebras, FOS: Mathematics, K-Theory and Homology (math.KT), Operator Algebras (math.OA)
Abstract: The goal of this paper is to solve the problem of existence of an $\ell^2$ relative eta morphism on the Higson-Roe structure group. Using the Cheeger-Gromov $\ell^2$ eta invariant, we construct a group morphism from the Higson-Roe maximal structure group constructed in [HiRo:10] to the reals. When we apply this morphism to the structure class associated with the spin Dirac operator for a metric of positive scalar curvature, we get the spin $\ell^2$ rho invariant. When we apply this morphism to the structure class associated with an oriented homotopy equivalence, we get the difference of the $\ell^2$ rho invariants of the corresponding signature operators. We thus get new proofs for the classical $\ell^2$ rigidity theorems of Keswani obtained in [Ke:00]., Comment: 40 pages; typos fixed, references added
Published: 2015

33. Magnetic properties and complex magnetic phase diagram in non centrosymmetric EuRhGe$_3$ and EuIrGe$_3$ single crystals

Author: Arvind Maurya, Pierre Bonville, Ruta Kulkarni, S. K. Dhar, A. Thamizhavel, Department of Condensed Matter Physics and Materials Science [TIFR] (CMPMS), Tata Institute for Fundamental Research (TIFR), Laboratoire Nano-Magnétisme et Oxydes (LNO), Service de physique de l'état condensé (SPEC - UMR3680), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Institut Rayonnement Matière de Saclay (IRAMIS), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, and Chennai Mathematical Institute [Inde]
Subjects: Materials science, EuRhGe$_3$, FOS: Physical sciences, 02 engineering and technology, Magnetic phase diagram, 01 natural sciences, Heat capacity, Condensed Matter - Strongly Correlated Electrons, Magnetization, Paramagnetism, Tetragonal crystal system, Phase (matter), 0103 physical sciences, 010306 general physics, Spin (physics), [PHYS]Physics [physics], $^{151}$Eu Mössbauer spectra, Condensed matter physics, Strongly Correlated Electrons (cond-mat.str-el), Single crystal, 021001 nanoscience & nanotechnology, Condensed Matter Physics, Electronic, Optical and Magnetic Materials, [PHYS.COND.CM-SCE]Physics [physics]/Condensed Matter [cond-mat]/Strongly Correlated Electrons [cond-mat.str-el], 0210 nano-technology, Current density, EuIrGe$_3$
Abstract: We report the magnetic properties of two Eu based compounds, single crystalline EuIrGe$_3$ and EuRhGe$_3$, inferred from magnetisation, electrical transport, heat capacity and $^{151}$Eu M\"{o}ssbauer spectroscopy. These previously known compounds crystallise in the non-centrosymmetric, tetragonal, $I4mm$, BaNiSn$_3$-type structure. Single crystals of EuIrGe$_3$ and EuRhGe$_3$ were grown using high temperature solution growth method using In as flux. EuIrGe$_3$ exhibits two magnetic orderings at $T_{\rm N1}$ = 12.4 K, and $T_{\rm N2}$ = 7.3 K. On the other hand EuRhGe$_3$ presents a single magnetic transition with a $T_{\rm N}$ = 12 K. $^{151}$Eu M\"{o}ssbauer spectra present evidence for a cascade of transitions from paramagnetic to incommensurate amplitude modulated followed by an equal moment antiferromagnetic phase at lower temperatures in EuIrGe$_3$, the transitions having a substantial first order character. On the other hand the $^{151}$Eu M\"{o}ssbauer spectra at 4.2 and 9 K in EuRhGe$_3$ present evidence of a single magnetic transition. In both compounds a superzone gap is observed for the current density $J\parallel$ [001], which enhances with transverse magnetic field. The magnetisation measured up to 14 T shows the occurrence of field induced transitions, which are well documented in the magnetotransport data as well. The magnetic phase diagram constructed from these data is complex, revealing the presence of many phases in the $H-T$ phase space.
Published: 2015
Full Text: View/download PDF

34. Sessions with an Unbounded Number of Agents

Author: Loïc Hélouët, Madhavan Mukund, Sundararaman Akshay, Department of Computer Science and Engineering [Bombay], Indian Institute of Technology Bombay (IIT Bombay), SUpervision of large MOdular and distributed systems (SUMO), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], Equipe associée DISTOL, DISTOL Assoicated team, LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Theoretical computer science, Business rule, Computer science, Semantics (computer science), 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, Sessions, 01 natural sciences, Operational semantics, Session (web analytics), Electronic mail, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, Server, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Chinese wall, Web service, verification, computer, WSTS, Web services
Abstract: In web-based business systems, agents engage in structured interactions, called sessions. Sessions are logical units of computations, like transactions. However, unlike transactions, sessions cannot be isolated from each other. Thus, one has to verify such systems in the presence of both intended and unintended interference between sessions. The main challenge in building a tractable model of sessions is that there is no a priori bound on the number of concurrently active agents and sessions in the system. Realistic specifications require agents to compare entities across sessions, but this has to be modelled without assigning an unbounded set of unique identities to active agents and sessions. We propose a model called session systems that allows for an arbitrary number of concurrently active agents and sessions. Agents are equipped with a limited ability to remember partners across sessions. Configurations are represented as graphs and the operational semantics is described through graph-rewriting. We show that, under reasonable restrictions, session systems are well-structured systems. This provides an effective verification algorithm for simple coverability properties. We then show how to use this result to verify more elaborate business rules such as avoidance of conflicts of interest and the Chinese Wall Property.; Dans les systèmes basés sur le Web, des agents interagissent au travers de protocoles prédéfinis appelés sessions. Les sessions sont des processus logiques, similaires à des transactions. Cependant, à la différence des transactions, des sessions sur le Web ne peuvent pas être entièrement encapsulées et isolées de leur environnement. Il faut donc s'assurer qu'un système utilisant des sessions ne comporte pas d'interférences indésirables. Un challenge pour concevoir un modèle de système orienté session est qu'il n'y a pas a priori de borne sur le nombre de sessions qui peuvent coexister au sein du système. la plupart des exemples réalistes imposent de savoir différencier deux sessions. Cependant, pour être utilisable, un modèle doit éviter de gérer des ensembles infinis d'identités d'agents et de sessions. Cet article propose un modèle appelé Session Systems, qui permet de modéliser un ensemble d'agents et de sessions de taille arbitraire. Les agents sont équipés d'une mémoire bornée leur permettant de mémoriser les identités d'autres agents. Les configurations de ce modèle sont représentées par des graphes, et la sémantique de notre modèle définie par des récritures de graphes. Nous montrons qu'avec une restriction raisonnables, les session systems sont des systèmes de transitions bien structurés. Ceci permet donne immédiatemetn des algorithmes pour vérifier des propriétés de couverture relativement simples, ou des propriétés plus complexes, telles que des règles commerciales : conflits d'intérêt ou muraille de Chine.
Published: 2014

35. Optimal bounds for parity-oblivious random access codes

Author: Jamie Sikora, Srijita Kundu, Iordanis Kerenidis, André Chailloux, Security, Cryptology and Transmissions (SECRET), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire d'informatique Algorithmique : Fondements et Applications (LIAFA), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), and Chennai Mathematical Institute [Inde]
Subjects: Semidefinite programming, Physics, Discrete mathematics, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Quantum Physics, business.industry, Open problem, FOS: Physical sciences, General Physics and Astronomy, Cryptography, 16. Peace & justice, 01 natural sciences, 010305 fluids & plasmas, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Quantum state, 0103 physical sciences, Quantum information, Quantum Physics (quant-ph), 010306 general physics, business, Quantum, Random access, Coding (social sciences), Computer Science::Cryptography and Security
Abstract: Random access coding is an information task that has been extensively studied and found many applications in quantum information. In this scenario, Alice receives an $n$-bit string $x$, and wishes to encode $x$ into a quantum state $\rho_x$, such that Bob, when receiving the state $\rho_x$, can choose any bit $i \in [n]$ and recover the input bit $x_i$ with high probability. Here we study two variants: parity-oblivious random access codes, where we impose the cryptographic property that Bob cannot infer any information about the parity of any subset of bits of the input apart from the single bits $x_i$; and even-parity-oblivious random access codes, where Bob cannot infer any information about the parity of any even-size subset of bits of the input. In this paper, we provide the optimal bounds for parity-oblivious quantum random access codes and show that they are asymptotically better than the optimal classical ones. Our results provide a large non-contextuality inequality violation and resolve the main open problem in a work of Spekkens, Buzacott, Keehn, Toner, and Pryde (2009). Second, we provide the optimal bounds for even-parity-oblivious random access codes by proving their equivalence to a non-local game and by providing tight bounds for the success probability of the non-local game via semidefinite programming. In the case of even-parity-oblivious random access codes, the cryptographic property holds also in the device-independent model., Comment: Version 3. Added discussion about device-independent security
Published: 2014

36. Distributed Timed Automata with Independently Evolving Clocks

Author: Benedikt Bollig, Madhavan Mukund, K. Narayan Kumar, Sundararaman Akshay, Paul Gastin, Department of Computer Science and Engineering [Bombay], Indian Institute of Technology Bombay (IIT Bombay), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Chennai Mathematical Institute [Inde]
Subjects: 0209 industrial biotechnology, Algebra and Number Theory, Theoretical computer science, Distributed computing, Timed automaton, 02 engineering and technology, Rate independent, Natural semantics, Theoretical Computer Science, Undecidable problem, Universality (dynamical systems), Automaton, 020901 industrial engineering & automation, Computational Theory and Mathematics, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, ComputingMilieux_MISCELLANEOUS, Information Systems, Mathematics
Abstract: We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to. There are two natural semantics for such systems. The universal semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. To check if a system avoids a negative specification, it is better to use the existential semantics---the set of behaviors that the system can possibly exhibit under some choice of clock rates. We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness or universality turns out to be undecidable. As an alternative to the universal semantics, we propose a reactive semantics that allows us to check positive specifications and yet describes a regular set of behaviors.
Published: 2014

37. Groupoids associated to semigroup actions

Author: Renault, Jean, Sundar, S., Mathématiques - Analyse, Probabilités, Modélisation - Orléans (MAPMO), Centre National de la Recherche Scientifique (CNRS)-Université d'Orléans (UO), and Chennai Mathematical Institute [Inde]
Subjects: Mathematics::Operator Algebras, MCS 22A22, Mathematics::Category Theory, [MATH.MATH-OA]Mathematics [math]/Operator Algebras [math.OA], FOS: Mathematics, Mathematics - Operator Algebras, Operator Algebras (math.OA), Wiener-Hopf C*-algebras
Abstract: 23 pages; In this paper, we consider topological semigroup actions on compact topological spaces. Under mild assumptions on the semigroup and the action, we construct a semi-direct product groupoid with a Haar system. We also show that it is equivalent to a transformation groupoid. We apply this construction to the Wiener-Hopf $C^{*}$-algebras.
Published: 2014

38. Verifying Communicating Multi-pushdown Systems

Author: Cyriac, Aiswarya, Gastin, Paul, Narayan Kumar, K., Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Chennai Mathematical Institute [Inde]
Subjects: Propositional Dynamic Logic, Under-approximate verification, Model-checking, Computer Science::Logic in Computer Science, Monadic Second-Order Logic, Concurrent systems, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Split-width, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; Communicating multi-pushdown systems model networks of multi-threaded recursive programs communicating via reliable FIFO channels. Hence their verification problems are undecidable in general. The behaviours of these systems can be represented as directed graphs, which subsume both Message Sequence Charts and nested words. We extend the notion of split-width to these graphs, defining a simple algebra to compose/decompose these behaviours using two natural operations: shuffle and merge. We obtain simple, uniform and optimal decision procedures for various verification problems parametrized by split-width, ranging from reachability to model-checking against MSO, PDL and Temporal Logics.
Published: 2014

39. On the Complexity of Trial and Error for Constraint Satisfaction Problems

Author: Raghav Kulkarni, Aarthi Sundaram, Youming Qiao, Miklos Santha, Gábor Ivanyos, Institute for Computer Science and Control [Budapest], Chennai Mathematical Institute [Inde], Institute for Theoretical Computer Science, Tsinghua University [Beijing] (THU), Centre National de la Recherche Scientifique (CNRS), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Centre for Quantum Technologies [Singapore] (CQT), National University of Singapore (NUS), and Tsinghua University [Beijing]
Subjects: [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], FOS: Computer and information sciences, Mathematical optimization, General Computer Science, Computational complexity theory, Computer Networks and Communications, 0102 computer and information sciences, 02 engineering and technology, Computer Science::Computational Complexity, Computational Complexity (cs.CC), 01 natural sciences, Oracle, Theoretical Computer Science, Computation Theory & Mathematics, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Artificial Intelligence & Image Processing, Graph property, Time complexity, Constraint satisfaction problem, ComputingMilieux_MISCELLANEOUS, Mathematics, 020203 distributed computing, Applied Mathematics, QA75 Electronic computers. Computer science / számítástechnika, számítógéptudomány, Trial and error, Constraint (information theory), Computer Science - Computational Complexity, Monotone polygon, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics
Abstract: In 2013 Bei, Chen and Zhang introduced a trial and error model of computing, and applied to some constraint satisfaction problems. In this model the input is hidden by an oracle which, for a candidate assignment, reveals some information about a violated constraint if the assignment is not satisfying. In this paper we initiate a {\em systematic} study of constraint satisfaction problems in the trial and error model. To achieve this, we first adopt a formal framework for CSPs, and based on this framework we define several types of revealing oracles. Our main contribution is to develop a \emph{transfer theorem} for each type of the revealing oracle, under a broad class of parameters. To any hidden CSP with a specific type of revealing oracle, the transfer theorem associates another, potentially harder CSP in the normal setting, such that their complexities are polynomial time equivalent. This in principle transfers the study of a large class of hidden CSPs, possibly with a promise on the instances, to the study of CSPs in the normal setting. We then apply the transfer theorems to get polynomial-time algorithms or hardness results for hidden CSPs, including satisfaction problems, monotone graph properties, isomorphism problems, and the exact version of the Unique Games problem. Most of the proofs of these results are short and straightforward, which exhibits the power of the transfer theorems., Comment: 26 pages. This is the final version that will appear in Journal of Computer and System Sciences
Published: 2014
Full Text: View/download PDF

40. Controllers for the Verification of Communicating Multi-Pushdown Systems

Author: C. Aiswarya, Paul Gastin, K. Narayan Kumar, Department of Information Technology (DIT-UPPSALA), Uppsala University, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Chennai Mathematical Institute [Inde]
Subjects: Class (computer programming), High-level verification, Functional verification, Computer science, Distributed computing, Verification, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Distributed controller, 0102 computer and information sciences, 02 engineering and technology, Construct (python library), 01 natural sciences, Decidability, Message sequence charts Multi-pushdown systems, 010201 computation theory & mathematics, restrict, Control theory, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Turing, computer, computer.programming_language
Abstract: International audience; Multi-pushdowns communicating via queues are formal models of multi-threaded programs communicating via channels. They are turing powerful and much of the work on their verification has focussed on under-approximation techniques. Any error detected in the under-approximation implies an error in the system. However the successful verification of the under-approximation is not as useful if the system exhibits unverified behaviours. Our aim is to design controllers that observe/restrict the system so that it stays within the verified under-approximation. We identify some important properties that a good con- troller should satisfy. We consider an extensive under-approximation class, construct a distributed controller with the desired properties and also establish the decidability of verification problems for this class.
Published: 2014

41. Constant Query Locally Decodable Codes against Computationally Bounded Adversary

Author: Bhattacharyya, Rishiraj, Chakraborty, Sourav, Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Arithmetic and Computing (ARIC), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Subjects: GeneralLiterature_REFERENCE(e.g.,dictionaries,encyclopedias,glossaries)
Abstract: Submitted
Published: 2013

42. Reasoning about Data Repetitions with Counter Systems

Author: Stéphane Demri, M. Praveen, Diego Figueira, Laboratoire Spécification et Vérification [Cachan] ( LSV ), École normale supérieure - Cachan ( ENS Cachan ) -Centre National de la Recherche Scientifique ( CNRS ), New York University ( NYU ), Laboratory for the Foundations of Computer Science [Edinburgh] ( LFCS ), University of Edinburgh, Laboratoire Bordelais de Recherche en Informatique ( LaBRI ), Centre National de la Recherche Scientifique ( CNRS ) -École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université Sciences et Technologies - Bordeaux 1-Université Bordeaux Segalen - Bordeaux 2, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), New York University [New York] (NYU), NYU System (NYU), Laboratory for the Foundations of Computer Science [Edinburgh] (LFCS), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Centre National de la Recherche Scientifique (CNRS), and Chennai Mathematical Institute [Inde]
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Class (set theory), Theoretical computer science, Reduction (recursion theory), General Computer Science, Matching (graph theory), Reachability problem, Computer science, 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], Upper and lower bounds, 01 natural sciences, Theoretical Computer Science, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Reachability, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Temporal logic, Mathematics, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Computability, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], F.3.1, F.4.1, F.4.3, [ INFO.INFO-DM ] Computer Science [cs]/Discrete Mathematics [cs.DM], Decision problem, Petri net, 16. Peace & justice, Satisfiability, Logic in Computer Science (cs.LO), [ INFO.INFO-DB ] Computer Science [cs]/Databases [cs.DB], 010201 computation theory & mathematics, [ INFO.INFO-FL ] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 020201 artificial intelligence & image processing, [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract: We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachability-like decision problems for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability/coverability problem in Petri nets. This gives us 2EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, a potentially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system., Comment: 54 pages
Published: 2013

43. Model Checking Parse Trees

Author: Sylvain Schmitz, Anudhyan Boral, Chennai Mathematical Institute [Inde], Laboratoire Spécification et Vérification [Cachan] (LSV), and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)
Subjects: FOS: Computer and information sciences, Model checking, Computer Science - Logic in Computer Science, Theoretical computer science, Computer science, media_common.quotation_subject, F.4, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Rule-based machine translation, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, PSPACE, media_common, D.3.1, Parsing, Grammar, I.2.7, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing), Syntax, NP, Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Dynamic logic (modal logic), Computational linguistics, computer
Abstract: Parse trees are fundamental syntactic structures in both computational linguistics and compilers construction. We argue in this paper that, in both fields, there are good incentives for model-checking sets of parse trees for some word according to a context-free grammar. We put forward the adequacy of propositional dynamic logic (PDL) on trees in these applications, and study as a sanity check the complexity of the corresponding model-checking problem: although complete for exponential time in the general case, we find natural restrictions on grammars for our applications and establish complexities ranging from nondeterministic polynomial time to polynomial space in the relevant cases., Comment: 21 + x pages
Published: 2013

44. Documenting Climate Models and Their Simulations

Author: Mark Morgan, Sébastien Denvil, Venkatramani Balaji, Karl E. Taylor, Bryan Lawrence, Sarah Callaghan, Eric Guilyardi, Sylvia Murphy, Michael Lautenschlager, Cecelia DeLuca, Variabilité climatique tropicale et globale (VARCLIM), Laboratoire d'Océanographie et du Climat : Expérimentations et Approches Numériques (LOCEAN), Muséum national d'Histoire naturelle (MNHN)-Institut de Recherche pour le Développement (IRD)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut national des sciences de l'Univers (INSU - CNRS)-Centre National de la Recherche Scientifique (CNRS)-Institut Pierre-Simon-Laplace (IPSL (FR_636)), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Université de Versailles Saint-Quentin-en-Yvelines (UVSQ)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Institut national des sciences de l'Univers (INSU - CNRS)-Université Paris Diderot - Paris 7 (UPD7)-École polytechnique (X)-Centre National d'Études Spatiales [Toulouse] (CNES)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Université de Versailles Saint-Quentin-en-Yvelines (UVSQ)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris Diderot - Paris 7 (UPD7)-École polytechnique (X)-Centre National d'Études Spatiales [Toulouse] (CNES)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Muséum national d'Histoire naturelle (MNHN)-Institut de Recherche pour le Développement (IRD)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut national des sciences de l'Univers (INSU - CNRS)-Centre National de la Recherche Scientifique (CNRS)-Institut Pierre-Simon-Laplace (IPSL (FR_636)), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Université de Versailles Saint-Quentin-en-Yvelines (UVSQ)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris Diderot - Paris 7 (UPD7)-École polytechnique (X)-Centre National d'Études Spatiales [Toulouse] (CNES)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], Institut Pierre-Simon-Laplace (IPSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Université de Versailles Saint-Quentin-en-Yvelines (UVSQ)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Institut national des sciences de l'Univers (INSU - CNRS)-École polytechnique (X)-Centre National d'Études Spatiales [Toulouse] (CNES)-Centre National de la Recherche Scientifique (CNRS), Institut de Recherche pour le Développement (IRD)-Centre National de la Recherche Scientifique (CNRS)-Institut national des sciences de l'Univers (INSU - CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Muséum national d'Histoire naturelle (MNHN)-Institut Pierre-Simon-Laplace (IPSL (FR_636)), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Université de Versailles Saint-Quentin-en-Yvelines (UVSQ)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Institut national des sciences de l'Univers (INSU - CNRS)-Université Paris Diderot - Paris 7 (UPD7)-École polytechnique (X)-Centre National d'Études Spatiales [Toulouse] (CNES)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris), and Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Université de Versailles Saint-Quentin-en-Yvelines (UVSQ)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris Diderot - Paris 7 (UPD7)-École polytechnique (X)-Centre National d'Études Spatiales [Toulouse] (CNES)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche pour le Développement (IRD)-Centre National de la Recherche Scientifique (CNRS)-Institut national des sciences de l'Univers (INSU - CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Muséum national d'Histoire naturelle (MNHN)-Institut Pierre-Simon-Laplace (IPSL (FR_636))
Subjects: Atmospheric Science, Coupled model intercomparison project, Government, 010504 meteorology & atmospheric sciences, business.industry, Management science, [SDU.STU.GP]Sciences of the Universe [physics]/Earth Sciences/Geophysics [physics.geo-ph], [SDE.MCG]Environmental Sciences/Global Changes, Environmental resource management, 0207 environmental engineering, Climate change, [PHYS.PHYS.PHYS-GEO-PH]Physics [physics]/Physics [physics]/Geophysics [physics.geo-ph], 02 engineering and technology, 01 natural sciences, Metadata repository, Metadata, Documentation, 13. Climate action, Climate model, 020701 environmental engineering, Adaptation (computer science), business, 0105 earth and related environmental sciences
Abstract: International audience; The results of climate models are of increasing and widespread importance. No longer is climate model output of sole interest to climate scientists and researchers in the climate change impacts and adaptation fields. Now nonspecialists such as government officials, policy makers, and the general public all have an increasing need to access climate model output and understand its implications. For this host of users, accurate and complete metadata (i.e., information about how and why the data were produced) is required to document the climate modeling results. Here we describe a pilot community initiative to collect and make available documentation of climate models and their simulations. In an initial application, a metadata repository is being established to provide information of this kind for a major internationally coordinated modeling activity known as CMIP5 (Coupled Model Intercomparison Project, Phase 5). It is expected that for a wide range of stakeholders, this and similar community-managed metadata repositories will spur development of analysis tools that facilitate discovery and exploitation of Earth system simulations.
Published: 2013

45. A quadratic construction for Zielonka automata with acyclic communication structure

Author: Anca Muscholl, Siddharth Krishna, Chennai Mathematical Institute [Inde], Laboratoire Bordelais de Recherche en Informatique (LaBRI), Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université Sciences et Technologies - Bordeaux 1-Université Bordeaux Segalen - Bordeaux 2, and Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)
Subjects: Discrete mathematics, Polynomial, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Theoretical computer science, General Computer Science, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, ω-automaton, 01 natural sciences, Theoretical Computer Science, Mobile automaton, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, DFA minimization, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, Automata theory, Graph (abstract data type), Quantum finite automata, Nondeterministic finite automaton, Computer Science::Formal Languages and Automata Theory, ComputingMilieux_MISCELLANEOUS, Mathematics
Abstract: Asynchronous automata are parallel compositions of finite-state processes synchronizing over shared variables. A deep theorem due to Zielonka says that every regular trace language can be recognized by a deterministic asynchronous automaton. The construction is rather involved and the most efficient variant produces automata which are exponential in the number of processes and polynomial in the size of the DFA. In this paper we show a simple, quadratic construction in the case where the synchronization actions are binary and define an acyclic communication graph.
Published: 2013

46. Better abstractions for timed automata

Author: Frédéric Herbreteau, Igor Walukiewicz, B. Srivathsan, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Chennai Mathematical Institute [Inde], Walukiewicz, Igor, and Herbreteau, Frédéric
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Theoretical computer science, Reachability problem, Computer science, Formal Languages and Automata Theory (cs.FL), Timed automaton, Parameterized complexity, Computer Science - Formal Languages and Automata Theory, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Theoretical Computer Science, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Reachability, 0202 electrical engineering, electronic engineering, information engineering, State space, Abstraction, Timed automata, Mathematics, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], reachability problem, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 16. Peace & justice, Search tree, Computer Science Applications, Automaton, Logic in Computer Science (cs.LO), Computational Theory and Mathematics, 010201 computation theory & mathematics, Automata theory, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, non-convex abstractions, Computer Science::Formal Languages and Automata Theory, Information Systems
Abstract: We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstractions preserve underlying simulation relations on the state space of the automaton. For both effectiveness and efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We consider the aLU abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets, it has not been used in implementations. We prove that aLU abstraction is the biggest abstraction with respect to LU-bounds that is sound and complete for reachability. We also provide an efficient technique to use the aLU abstraction to solve the reachability problem., Comment: Extended version of LICS 2012 paper (conference paper till v6). in Information and Computation, available online 27 July 2016
Published: 2012

47. Model Checking Languages of Data Words

Author: Benedikt Bollig, Aiswarya Cyriac, K. Narayan Kumar, Paul Gastin, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Chennai Mathematical Institute [Inde], and Lars Birkedal
Subjects: Discrete mathematics, Model checking, Theoretical computer science, Transitive closure, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Predicate (mathematical logic), 16. Peace & justice, 01 natural sciences, Satisfiability, Automaton, Undecidable problem, Identifier, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Word (computer architecture), Computer Science::Formal Languages and Automata Theory, Mathematics
Abstract: International audience; We consider the model-checking problem for data multi-pushdown automata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic second-order (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as first-order logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic.
Published: 2012

48. Unidirectional Channel Systems Can Be Tested

Author: Petr Jancar, Prateek Karandikar, Philippe Schnoebelen, Technical University of Ostrava [Ostrava] (VSB), Chennai Mathematical Institute [Inde], Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Jos C. M. Baeten, Tom Ball, Frank S. Boer, TC 1, TC 2, and WG 2.2
Subjects: Reachability problem, FIFO (computing and electronics), 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Decidability, Undecidable problem, Embedding problem, Regular language, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Communication source, Algorithm, Computer Science::Formal Languages and Automata Theory, Computer Science::Information Theory, Communication channel, Mathematics
Abstract: International audience; “Unidirectional channel systems” (Chambart & Schnoebelen, CONCUR 2008) are systems where one-way communication from a sender to a receiver goes via one reliable and one unreliable (unbounded fifo) channel. Equipping these systems with the possibility of testing regular properties on the contents of channels makes verification undecidable. Decidability is preserved when only emptiness and nonemptiness tests are considered: the proof relies on a series of reductions eventually allowing us to take advantage of recent results on Post’s Embedding Problem.
Published: 2012

49. MSO Decidability of Multi-Pushdown Systems via Split-Width

Author: Aiswarya Cyriac, K. Narayan Kumar, Paul Gastin, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Chennai Mathematical Institute [Inde], Koutny, Maciej and Ulidowski, and Irek
Subjects: Discrete mathematics, Sequence, Nested word, Matching (graph theory), Binary relation, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Recursion (computer science), 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Decidability, Combinatorics, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, Tree automaton, Computer Science::Formal Languages and Automata Theory, Mathematics, Merge (linguistics)
Abstract: International audience; Multi-threaded programs with recursion are naturally modeled as multi-pushdown systems. The behaviors are represented as multiply nested words (MNWs), which are words enriched with additional binary relations for each stack matching a push operation with the corresponding pop operation. Any MNW can be decomposed by two basic and natural operations: shuffle of two sequences of factors and merge of consecutive factors of a sequence. We say that the split-width of a MNW is k if it admits a decomposition where the number of factors in each sequence is at most k. The MSO theory of MNWs with split-width k is decidable. We introduce two very general classes of MNWs that strictly generalize known decidable classes and prove their MSO decidability via their split-width and obtain comparable or better bounds of tree-width of known classes.
Published: 2012

50. Uncertainty principles for the Schrödinger equation on Riemannian symmetric spaces of the noncompact type

Author: A. Pasquale, Maddala Sundari, Laboratoire de Mathématiques et Applications de Metz (LMAM), Centre National de la Recherche Scientifique (CNRS)-Université Paul Verlaine - Metz (UPVM), and Chennai Mathematical Institute [Inde]
Subjects: Uncertainty principle, Schrödinger equation, Helgason-Fourier transform, Type (model theory), Riemannian geometry, 01 natural sciences, symbols.namesake, 0103 physical sciences, Initial value problem, Beurling theorem, 0101 mathematics, [MATH]Mathematics [math], Mathematics, Algebra and Number Theory, 010102 general mathematics, Mathematical analysis, Zero (complex analysis), Square-integrable function, Symmetric space, symbols, 010307 mathematical physics, Geometry and Topology, 43A85, 58Jxx, Hardy theorem
Abstract: International audience; Let X be a Riemannian symmetric space of the noncompact type. We prove that the solution of the time-dependent Schrödinger equation on X with square integrable initial condition f is identically zero at all times t whenever f and the solution at a time t 0 >0 are simultaneously very rapidly decreasing. The stated condition of rapid decrease is of Beurling type. Conditions respectively of Gelfand-Shilov, Cowling-Price and Hardy type are deduced.
Published: 2012

Catalog

Books, media, physical & digital resources

See catalog results

Searchworks

Select search scope, currently: Articles Catalog books, media & more in Jio Institute collections Articles journal articles & other e-resources

Search

Search Constraints

Refine your results

Search Limiters

Topic

Publication Year Range

Language

Journal

Database

Publisher

52 results on '"Chennai Mathematical Institute [Inde]"'

Search Results

Catalog

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources