arXiv:2209.09333v1 [cs.FL] 19 Sep 2022

DOI: 10.4204/EPTCS.370
ISSN: 2075-2180

EPTCS 370

Proceedings of the 13th International Symposium on
Games, Automata, Logics and Formal Verification
Madrid, Spain, September 21-23, 2022

Edited by: Pierre Ganty and Dario Della Monica

Preface
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

Preface

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

Program Chairs

Program Committee

Steering Committee

External Reviewers

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.


Techniques for Unambiguous Systems

Wojciech Czerwiński (University of Warsaw, Poland)

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.


Learning Languages of Infinite Words

Dana Fisman (Ben-Gurion University, Israel)

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.


State Complexity of Population Protocols

Javier Esparza (Technische Universität München, Germany)

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.


Towards Multiset Semantics Database Theory: How I Learned to Stop Worrying and Love Linear Algebra

Jerzy Marcinkowski (University of Wrocław, Poland)

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.