Published: 20th September 2020 DOI: 10.4204/EPTCS.326 ISSN: 2075-2180 |
Preface Jean-Francois Raskin and Davide Bresolin | |
Invited Presentation:
Probabilistic Hyperproperties Erika Ábrahám | |
Invited Presentation:
Three Modern Roles for Logic in AI Adnan Darwiche | |
Invited Presentation:
Approximating Values of Generalized-Reachability Stochastic Games Jan Křetínský | |
Invited Presentation:
Regret Minimization in Discounted-Sum Games Guillermo Perez | |
LTLf Synthesis under Partial Observability: From Theory to Practice Lucas M. Tabajara and Moshe Y. Vardi | 1 |
Symbolic Parity Game Solvers that Yield Winning Strategies Oebele Lijzenga and Tom van Dijk | 18 |
Synthesis in Presence of Dynamic Links Béatrice Bérard, Benedikt Bollig, Patricia Bouyer, Matthias Függer and Nathalie Sznajder | 33 |
Symbolic Execution + Model Counting + Entropy Maximization = Automatic Search Synthesis Mara Downing, Abtin Molavi and Lucas Bang | 50 |
A Game Theoretical Semantics for Logics of Nonsense Can Başkent | 66 |
Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants Lauri Hella, Antti Kuusisto and Raine Rönnholm | 82 |
Local Higher-Order Fixpoint Iteration Florian Bruse, Jörg Kreiker, Martin Lange and Marco Sälzer | 97 |
Optimal Strategies in Weighted Limit Games Aniello Murano, Sasha Rubin and Martin Zimmermann | 114 |
Comparison of Algorithms for Simple Stochastic Games Jan Křetínský, Emanuel Ramneantu, Alexander Slivinskiy and Maximilian Weininger | 131 |
Decisiveness of Stochastic Systems and its Application to Hybrid Models Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière and Pierre Vandenhove | 149 |
LTLf Synthesis on Probabilistic Systems Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki and Moshe Y. Vardi | 166 |
On the Power of Unambiguity in Büchi Complementation Yong Li, Moshe Y. Vardi and Lijun Zhang | 182 |
Canonicity in GFG and Transition-Based Automata Bader Abu Radi and Orna Kupferman | 199 |
The Quotient in Preorder Theories Íñigo X. Íncer Romeo, Leonardo Mangeruca, Tiziano Villa and Alberto Sangiovanni-Vincentelli | 216 |
This volume contains the proceedings of the 11th International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2020). The symposium took place as a fully online event on September 21-22, 2020.
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. 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 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 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 Erika Abraham (RWTH Aachen, Germany), Adnan Darwiche (UCLA, USA), Jan Kretinsky (TU München, Germany), and Guillermo Perez (U Antwerpen, Belgium).
We wish to express our thanks 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.
Jean-François Raskin and Davide Bresolin
Davide Bresolin, University of Padova (Italy)
Jean-François Raskin, Université libre de Bruxelles (Belgium)
Alessandro Abate, University of Oxford (UK)
Galit Ashkenazi-Golan, Tel-Aviv university (Israel)
Benedikt Bollig, ENS Cachan, CNRS (France)
Pedro Cabalar, University of Corunna (Spain)
Franck Cassez, Macquarie University (Australia)
Silvia Crafa, Università di Padova (Italy)
Rüdiger Ehlers, Clausthal University of Technology (Germany)
Mohamed Faouzi Atig, Uppsala University (Sweden)
János Flesch , Maastricht University (The Netherlands)
Jan Kretinsky, Technical University of Munich (Germany)
Orna Kupferman, Hebrew University (Israel)
Sławomir Lasota, Warsaw University (Poland)
Ranko Lazic, University of Warwick (UK)
Jérôme Leroux, University of Bordeaux (France)
Radu Mardare, University of Strathclyde (UK)
Angelo Montanari, University of Udine (Italy)
Emilio Muñoz-Velasco, University of Malaga (Spain)
Gennaro Parlato, University of Molise (Italy)
Mickael Randour, Université de Mons (Belgium)
Sriram Sankaranarayanan, University of Colorado (USA)
B Srivathsan, Chennai Mathematical Institute (India)
Martin Zimmermann, University of Liverpool (UK)
Luca Aceto (Reykjavik University, Iceland)
Javier Esparza (University of Munich, Germany)
Salvatore La Torre (University of Salerno, Italy)
Angelo Montanari (University of Udine, Italy)
Mimmo Parente (University of Salerno, Italy)
Wolfgang Thomas (Aachen University, Germany)
Lorenzo Clemente, Daniele Dell'Erba, Alessandro Facchini, Anna Lisa Ferrara, Luca Geatti, Julian Gutierrez, Piotr Hofman, Karoliina Lehtinen, Gethin Norman, Arno Pauly, Gabriele Puppis, Arnaud Sangnier, Amrita Suresh, S P Suresh, Damian Szmuc, Pierre Vandenhove, Maximilian Weininger
Four decades ago, Lamport used the notion of trace properties as a means to specify the correctness of individual executions of concurrent programs. This notion was later formalized and classified by Alpern and Schneider to safety and liveness properties. Temporal logics like LTL and CTL were built based on these efforts to give formal syntax and semantics to requirements of trace properties. Subsequently, verification algorithms were developed to reason about individual executions of a system.
However, it turns out that many interesting requirements are not trace properties. For example, important information-flow security policies (e.g. noninterference, observational determinism) or service level agreements (e.g. mean response time, percentage uptime) cannot be expressed as properties of individual execution traces of a system. Rather, they are properties of sets of execution traces, also known as hyperproperties. Temporal logics such as HyperLTL and HyperCTL* have been proposed to provide a unifying framework to express and reason about hyperproperties.
This talk is devoted to special class of hyperproperties: we ask the question what are hyperproperties in the context of systems with random behavior. We will discuss what are relevant probabilistic relations between independent executions of a system, how we can formally express them in a temporal logic, and how we can decide the truth of such statements.
I will discuss three modern roles for logic in artificial intelligence, which are based on the theory of tractable Boolean circuits: (1) logic as a basis for computation, (2) logic for learning from a combination of data and knowledge, and (3) logic for reasoning about the behavior of machine learning systems.
Simple stochastic games are turn-based two-and-a-half-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. Here we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound.
Discounted-sum games provide a formal model for the study of reinforcement learning, where the agent is enticed to get rewards early since later rewards are discounted. When the agent interacts with the environment, she may realize that, with hindsight, she could have increased her reward by playing differently: this difference in outcomes constitutes her regret value. The agent may thus elect to follow a regret- minimal strategy. In this talk, we will see that (1) there always exist regret-minimal strategies that are admissible—a strategy being inadmissible if there is another strategy that always performs better; (2) computing the minimum possible regret or checking that a strategy is regret-minimal can be done in coNP with an NP oracle, disregarding the computational cost of numerical analysis (otherwise, this bound becomes PSPACE). Finally, we will give a brief overview of other related problems that we have studied and some interesting problems that remain open.