|
Published: 30th September 2023 DOI: 10.4204/EPTCS.390 ISSN: 2075-2180 |
This volume contains the proceedings of GandALF 2023, the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification. The symposium was held in Udine, Italy, on September 18-20, 2023.
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 Madrid, Spain (2022); 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 committees and by the country distribution of the submitted papers.
The program committee selected 15 papers (out of 26 submissions) for presentation at the symposium. Each paper was reviewed by at least three 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 and automata learning, logics for computer science and verification, computational and descriptive complexity theory, formal methods and specification languages, concurrency and process semantics, games, strategic reasoning, and synthesis. The program included four invited talks, given by Laure Daviaud (University of East Anglia, UK), Juha Kontinen (University of Helsinki, Finland), Sophie Pinchinat (IRISA/University of Rennes, France), and Alexander Rabinovich (Tel Aviv University, Israel). 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 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: Andrea Brunello, Renato Acampora, Luca Geatti, Nicola Gigante, Mattia Guiotto, Gabriele Puppis, and Nicola Saccomanno for making sure the event ran smoothly.
Antonis Achilleos and Dario Della Monica
Daniel Thoma, Dylan Bellier, Nikos Tzevelekos, Massimiliano Goldwurm, Luca Prigioniero, Bernd Gärtner, Masaki Waga, Reijo Jaakkola, Carlo Mereghetti, Riccardo Romanello, Tomoyuki Yamakami, Anatole Dahan, Daniele Dell’Erba, Lorenzo Clemente, Duligur Ibeling, Martin Sachenbacher, and William Farmer.
Team Semantics is the mathematical basis of modern logics for reasoning about dependence, independence, and imperfect information. During the past decade research on team semantics has flourished with interesting connections to fields such as database theory, statistics, formal linguistics, hyperproperties and causality, just to mention a few examples. I will give a short introduction to first-order team semantics and review the expressivity and complexity of the most prominent logics of the area. I will also discuss probabilistic variants of these logics and their connections to the existential theory of the reals.
In this talk I will review some results about weighted automata: what is decidable (or not) when it comes to describing their behaviour and what are the mathematical tools that are used to prove such results. In particular, I will describe Simon’s factorisation theorem, how it plays a major role in several of these results and how it could be used more widely.
Church’s Problem asks for the construction of a procedure which, given a logical specification φ(I, O) between input ω-strings I and output ω-strings O, determines whether there exists an operator F that implements the specification in the sense that φ(I, F(I)) holds for all inputs I. Büchi and Landweber gave a procedure to solve Church’s problem for MSO specifications and operators computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time of the non-negative reals. It turns out that in the continuous time there are phenomena which are very different from the canonical discrete time domain of the natural numbers.
We first briefly survey various formal settings for Strategic Reasoning under Imperfect Information in multi-player games. From the point of view of automated verification and/or synthesis, we motivate the assumption of Synchronous Recall, that enforces particular properties on players’ observation capabilities.
Second, with the focus on aforementioned Synchronous Recall assumption, we consider arenas that arise from Dynamic Epistemic Logic, a modal logic dedicated to specifying information changes in a multi-player game. Such arenas are described in a symbolic manner, with an initial epistemic state and rules for player moves to attain new epistemic state, thus reflecting the information change that takes place.
We then explain how such symbolic arenas denote a possibly infinite first-order structure - reminiscent of the trees considered for interpreting Epistemic Temporal Logic. Second, we exploit this angle of view to go through the current state-of-the-art for reasoning (including planning) about these structures, and analyse the frontier of this overall setting regarding Strategic Reasoning.