|
Published: 17th September 2021 DOI: 10.4204/EPTCS.346 ISSN: 2075-2180 |
This volume contains the proceedings of GandALF 2021, the Twelfth International Symposium on Games, Automata, Logics, and Formal Verification. The symposium was held both online and in Padua, Italy, from September 20 to 22, 2021. The GandALF Symposium was co-located with the 3rd OVERLAY Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis.
The GandALF symposium was established by a group of Italian computer scientists to provide an opportunity for researchers interested in mathematical logic, 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 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 19 papers (out of 39 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 contained presentations on automata and transition systems, stochastic and quantitative models, game logic, temporal logic, synthesis algorithms and tools. The program included four invited talks given by Roderick Bloem (TU Graz, Austria), Anca Muscholl (LaBRI, Bordeaux, France), Nicola Olivetti (Aix-Marseille University, France), and S.E. (Sicco) Verwer (TU Delft, The Netherlands).
We are deeply grateful to the authors who submitted papers for consideration, to the speakers, to the program committee members and the additional reviewers for their excellent work. We also thank the EasyChair organization for supporting all the tasks related to the selection of contributions, and EPTCS and arXiv for hosting the proceedings.
Davide Bresolin and Pierre Ganty
Anantha Padmanabha, Andrey Rivkin, Andrzej Zbrzezny, Antonio Casares, Arnaud Sangnier, Benedikt Bollig, Clément Tamines, Daniela Petrisan, Daniele Dell’Erba, Didier Lime, Florian Bruse, Florian Furbach, Francesco Parolini, Grzegorz Fabiański, Johannes Doleschal, Jovan Komatovic, Jérémy Ledent, K. Narayan Kumar, Lorenzo Clemente, Louis-Marie Dando, Marco Zanella, Michał Skrzypczak, Nathanaël Fijalkow, Parreaux Julie, Pascal Fontaine, Paweł Parys, Prakash Saivasan, Prathamesh Turaga, S. Akshay, Sarah Winkler, Satoshi Masuya, Sebastian Wolff, Sparsa Roychowdhury, Sören van der Wall, Thomas Haas.
Deterministic, sound negotiations represent a tractable distributed model related to Petri nets and Zielonka automata. We describe in this talk how to exploit the structure of sound negotiations in order to derive polynomial-time algorithms, avoiding the state explosion induced by configurations. We also explain how to obtain polynomial-time Angluin-style algorithms for active learning of sound negotiations. (This is joint work with I. Walukiewicz.)
Non-normal modal logics (NNML) are known since a long time. They are a generalisation of standard normal modal logics, that do not satisfy some basic principles of them, in some cases they even contradict them. NNML have been studied mainly by philosophers for overcoming difficulties and paradoxes of epistemic and deontic reasoning originated by their formalisation in normal modal logics.
In my opinion the interest of NNML has not been fully recognised in Knowledge Representation, not only for epistemic and deontic reasoning, but also for reasoning about agency and capability.
One possible reason that hindered their larger use is the rather abstract Neighbourhood semantics which comes with them, as well as the lack of efficient and “friendly” proof systems.
The aim of my talk is to vindicate Non Normal modal logics, suggesting also a natural reformulation of their semantics and recent developments in their proof theory.
State machine learning deals with the problem of reconstructing a state machine (automaton) model from sequences of observations. In the standard use-case, we have access to the input and output events from a software component and the goal is to find a small model describing the mapping from inputs to outputs. In more complex settings, we observe only inputs, only have access to indirect signals from e.g. sensors, or sometimes we may have white-box access to the system. In this talk, I will show examples of standard and complex settings and how to setup Flexfringe to learn models in each of these cases. I will also demonstrate how the obtained models can be used in further processes such as finding bugs and safety verification. A special focus is on the trade-off between predictive accuracy and interpretability of these models. Reverse engineering models of systems is often performed for interpretability while the learning algorithms focus on accuracy. I will present initial ideas on how to modify this learning objective and results we obtained using it.
You have a reinforcement learning system? Sure, it works great, but does it give you any guarantees? I thought not.
We will describe methods to use reactive synthesis to construct runtime enforcement modules (shields) that can ensure that a system works correctly, even if the system has bugs. If the system doesn’t have too many bugs, the behavior of the shielded system will stay close to the behavior of the original system. We will show extensions to probabilistic and timed settings.