Published: 20th September 2022|
|Invited Presentation: Techniques for Unambiguous Systems Wojciech Czerwiński|
|Invited Presentation: Learning Languages of Infinite Words Dana Fisman|
|Invited Presentation: State Complexity of Population Protocols Javier Esparza|
|Invited Presentation: Towards Multiset Semantics Database Theory: How I Learned to Stop Worrying and Love Linear Algebra Jerzy Marcinkowski|
|On the Existential Fragments of Local First-Order Logics with Data Benedikt Bollig, Arnaud Sangnier and Olivier Stietel||1|
|Capturing Bisimulation-Invariant Exponential-Time Complexity Classes Florian Bruse, David Kronenberger and Martin Lange||17|
|Complexity through Translations for Modal Logic with Recursion Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza and Anna Ingolfsdottir||34|
|Schema-Based Automata Determinization Joachim Niehren, Momar Sakho and Antonio Al Serhali||49|
|Generating Tokenizers with Flat Automata Hans de Nivelle and Dina Muktubayeva||66|
|Analyzing Robustness of Angluin's L* Algorithm in Presence of Noise Igor Khmelnitsky, Serge Haddad, Lina Ye, Benoît Barbot, Benedikt Bollig, Martin Leucker, Daniel Neider and Rajarshi Roy||81|
|Parametric Interval Temporal Logic over Infinite Words Laura Bozzelli and Adriano Peron||97|
|Realizable and Context-Free Hyperlanguages Hadar Frenkel and Sarai Sheinvald||114|
|Controller Synthesis for Timeline-based Games Renato Acampora, Luca Geatti, Nicola Gigante, Angelo Montanari and Valentino Picotti||131|
|CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms Dalton Chichester, Wei Du, Raymond Kauffman, Hai Lin, Christopher Lynch, Andrew M. Marshall, Catherine A. Meadows, Paliath Narendran, Veena Ravishankar, Luis Rovira and Brandon Rozek||147|
|Adversarial Formal Semantics of Attack Trees and Related Problems Thomas Brihaye, Sophie Pinchinat and Alexandre Terefenko||162|
|Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets Giann Karlo Aguirre-Samboní, Stefan Haar, Loïc Paulevé, Stefan Schwoon and Nick Würdemann||178|
|Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types Felix Stutz and Damien Zufferey||194|
|Characterizing the Decidability of Finite State Automata Team Games with Communication Michael Coulombe and Jayson Lynch||213|
This volume contains the proceedings of GandALF 2022, the Thirteenth International Symposium on Games, Automata, Logics, and Formal Verification. The symposium was held in Madrid, Spain, September 21-23, 2022.
The GandALF symposium was established by a group of Italian computer scientists to provide an opportunity for researchers interested in logic for computer science, automata theory, game theory, to gather and discuss the application of formal methods to the specification, design, and verification of complex systems. Previous editions of GandALF were held in Padova, Italy (2021); Brussels, Belgium (2020); Bordeaux, France (2019); Saarbrücken, Germany (2018); Rome, Italy (2017); Catania, Italy (2016); Genoa, Italy (2015); Verona, Italy (2014); Borca di Cadore, Italy (2013); Napoli, Italy (2012); and Minori, Italy (2011 and 2010). It is a forum where people from different areas, and possibly with different backgrounds, can fruitfully interact, with a truly international spirit, as witnessed by the composition of the program and steering committee and by the country distribution of the submitted papers.
The program committee selected 14 papers (out of 20 submissions) for presentation at the symposium. Each paper was reviewed by at least two referees, and the selection was based on originality, quality, and relevance to the topics of the call for papers. The scientific program included presentations on automata, logics for computer science and verification, complexity theory, formal methods and languages, games, synthesis algorithms and security. The program included four invited talks, given by Wojciech Czerwiński (University of Warsaw, Poland), Javier Esparza (Technische Universität München, Germany), Dana Fisman (Ben-Gurion University, Israel), and Jerzy Marcinkowski (University of Wrocław, Poland). We are deeply grateful to them for contributing to this year edition of GandALF.
We would like to thank the authors who submitted papers for consideration, the speakers, the program committee members and the additional reviewers for their excellent work. We also thank Eddie Kohler for the HotCRP conference review software, EPTCS and arXiv for hosting the proceedings; in particular, we thank Rob van Glabbeek for the precise and prompt technical support with issues related with the proceeding publication procedure.
Finally we would like to thank the local organisers, and especially Tania Rodríguez and María Alcaraz for making sure the event ran smoothly.
Dario Della Monica and Pierre Ganty
Adriano Peron, Adrien Pommellet, Antoine Mottet, Bartosz Klin, Eryk Kopczyński, Gaëtan Staquet, Giannicola Scarpa, Ji Guan, Joseph Lallemand, Loïc Hélouët, Moses Ganardi, Ramanathan Srinivasan, Sylvain Lombardy, and Wanwei Liu.
In recent years it became apparent that many decision problems can be solved efficiently on unambiguous systems (systems in which each word is accepted by at most one run). I will show first a classical approach for solving language equivalence by weighted automata. Then I will present novel techniques, which helped us solve the problem for vector addition systems. Finally I plan to advertise an interesting related problem of multiplicity equivalence, which seems to reveal some connections between the unambiguity problem and other fields of mathematics.
The problem of inferring an automaton model of a black box system has found many applications in formal methods of system design. If the black-box system implements (or can be abstracted as) a regular language of finite words, it can be inferred in polynomial time using query learning. In this talk we'll discuss the problem we face when the black-box system implements a regular language of infinite words (e.g. the black-box is a reactive system).
While there are automata processing infinite words e.g. (Buechi automata) that have the same structure as automata on finite words (DFAs), learning them seems to be a harder problem. During the talk we will get acquainted with the ideas behind learning algorithms for regular languages, the obstacles in devising learning algorithms for regular languages of infinite words, and state-of-the-art results on learnability of acceptors of regular languages of infinite words.
Population protocols were introduced by Angluin et al. in 2004 to study the theoretical properties of networks of mobile sensors with very limited computational resources. They have also been proposed as a natural computing model, with molecules, cells, or microorganisms playing the role of sensors.
In a population protocol an arbitrary number of indistinguishable, finite-state agents interact randomly in pairs to collectively decide if their initial global configuration satisfies a given property. The property is formalized as a predicate that maps each initial configuration to an output, 0 or 1. Starting from an initial configuration, the agents eventually agree to the correct output almost surely, and continue producing it forever. The protocol is said to stabilize to the correct output.
Population protocols can decide exactly the semilinear predicates, or, equivalently, the predicates expressible in Presburger arithmetic. Current research concentrates on investigating the amount of resources needed to decide a given predicate. The standard resources, time and memory, translate for population protocols into expected time to stabilization and number of states of each agent. In this talk we concentrate on the state complexity of population protocols, for which matching upper and lower bounds have been found in the last few years.
For the last ten years, or maybe more, I have been a Database Theorist.
Like all (or at least most of) the Database Theorists I modelled the real-world-database relations, and real-world answers to the queries, as sets. If my query was "Exists y Cat(y) and Owns(x,y)", and my database happened to contain the tuples "Cat(Tibby)" and "Owns(Andreas, Tibby)" then -- clearly -- the constant "Andreas" was an element of the answer set.
I studied this model, using the methodology of mathematics. My toolbox was simple. It comprised some specific Database Theory concepts (like Chase) and some simple Computation Theory tricks (including maybe some automata-based arguments). Using this toolbox I constructed reasonings, which were occasionally complicated, but always elementary. It was fun.
But then, in early 2021, someone asked me what would happen to my results concerning Query Determinacy (whatever it is) if I considered a more realistic model, in which database relations, and answers to the queries, are multisets rather than sets. So, if my database knew that Andreas actually has six cats, the answer (multi)set would contain the constant "Andreas" with multiplicity six.
We started to think about it (with my very clever students, Jarosław Kwiecień and Piotr Ostropolski-Nalewaja) and soon we realized that this minor change in the assumptions about the model leads to a major change in the tools we need to study it. This felt to us like entering a completely new world. Suddenly the language and the methods from Linear Algebra appear so naturally that it is fair to say that they impose themselves on the researchers.
Clearly, we were not the first Database Theorists to set foot on this new continent. People have attempted to re-examine old Database Theory results, in the multiset-semantics scenario, for about 30 years now. But such attempts were few. And this is (I guess) exactly because in order to make any progress here one needs to learn totally new tools.
To our surprise we learned that this continent had also been visited before by the Mathematicians. They had constructed a number of structures there, some of them of some use for us. That's a bit frustrating, because they use different terms to call some notions, and it is not always straightforward to understand how to translate their own results to our language.
My talk will be a story by a traveller astonished by what he saw during his first short trip to the little known continent of Multiset-Semantics Database Theory.
To give you a glimpse of the techniques that appear there I will present some results and arguments from our PODS 2022 paper "Determinacy of Real Conjunctive Queries. The Boolean Case" (with Kwiecień and Ostropolski-Nalewaja). But I will also mention the adventures of other travellers to this new land, with particular emphasis on the famous Conjunctive Query Containment Problem.