Official versions can be found under the DOI reference while extended technical reports are available as an arXiv/.pdf link.
Alessandro Abate, Julian Gutierrez, Lewis Hammond, Paul Harrenstein, Marta
Kwiatkowska, Muhammad Najib, Giuseppe Perelli, Thomas Steeples, and
Michael J. Wooldridge.
Rational verification: game-theoretic verification of multi-agent
Applied Intelligence, 2021.
[ DOI |
We provide a survey of the state of the art of rational verification: the problem of checking whether a given temporal logic formula ϕ is satisfied in some or all game-theoretic equilibria of a multi-agent system – that is, whether the system will exhibit the behavior ϕ represents under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the overall framework of rational verification, we discuss key results obtained in the past few years as well as relevant related work in logic, AI, and computer science.
Julian Gutierrez, Lewis Hammond, Anthony W. Lin, Muhammad Najib, and Michael J.
Rational Verification for Probabilistic Systems.
to appear in KR, 2021.
[ arXiv ]
Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational verification problem for both non-cooperative games and cooperative games in the qualitative probabilistic setting. In the former case, we consider LTL properties satisfied by the Nash equilibria of the game and in the latter case LTL properties satisfied by the core. In both cases, we show that the problem is 2EXPTIME-complete, thus not harder than the much simpler verification problem of model checking LTL properties of systems modelled as Markov decision processes (MDPs).
Learning Union of Integer Hypercubes with Queries.
Oliver Markgraf, Daniel Stan, and Anthony W. Lin.
In CAV 2021.
[ DOI |
We study the problem of learning a finite union of integer (axis-aligned) hypercubes over the d-dimensional integer lattice, i.e., whose edges are parallel to the coordinate axes. This is a natural generalization of the classic problem in the computational learning theory of learning rectangles. We provide a learning algorithm with access to a minimally adequate teacher (i.e. membership and equivalence oracles) that solves this problem in polynomial-time, for any fixed dimension d. Over a non-fixed dimension, the problem subsumes the problem of learning DNF boolean formulas, a central open problem in the field. We have also provided extensions to handle infinite hypercubes in the union, as well as showing how subset queries could improve the performance of the learning algorithm in practice. Our problem has a natural application to the problem of monadic decomposition of quantifier-free integer linear arithmetic formulas, which has been actively studied in recent years. In particular, a finite union of integer hypercubes correspond to a finite disjunction of monadic predicates over integer linear arithmetic (without modulo constraints). Our experiments suggest that our learning algorithms substantially outperform the existing algorithms.
Regular Model Checking Approach to Knowledge Reasoning over Parameterized
Daniel Stan and Anthony W. Lin.
In AAMAS 2021.
[ arXiv |
We present a general framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In our framework, the number of agents or the amount of certain resources are parameterized (i.e. not known a priori), and the corresponding verification problem asks whether a given epistemic property is true regardless of the instantiation of the parameters. For example, in a muddy children puzzle, one could ask whether each child will eventually find out whether (s)he is muddy, regardless of the number of children. Our framework is regular model checking (RMC)-based, wherein synchronous finite-state automata (equivalently, monadic second-order logic over words) are used to specify the systems. We propose an extension of public announcement logic as specification language. Of special interests is the addition of the so-called iterated public announcement operators, which are crucial for reasoning about knowledge in parameterized systems. Although the operators make the model checking problem undecidable, we show that this becomes decidable when an appropriate "disappearance relation" is given. Further, we show how Angluin's L*-algorithm for learning finite automata can be applied to find a disappearance relation, which is guaranteed to terminate if it is regular. We have implemented the algorithm and apply this to such examples as the Muddy Children Puzzle, the Russian Card Problem, and Large Number Challenge.
Keywords: automaton learning, epistemic, parameterised, regular model checking, muddy children, public announcement logic
|||Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif. Intell., 287:103353, 2020. [ DOI | arXiv | http ]|
|||Anthony W. Lin and Philipp Rümmer. Regular model checking revisited (technical report). CoRR, abs/2005.00990, 2020. [ arXiv | http ]|
|||Monadic Decomposition in Integer Linear Arithmetic. Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I. [ DOI | arXiv | http ]|
|||A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, and Zhilin Wu. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. [ DOI | arXiv | http ]|
|||Parameterized Synthesis with Safety Properties. Oliver Markgraf, Chih-Duo Hong, Anthony W. Lin, Muhammad Najib, and Daniel Neider. In Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings. [ DOI | arXiv | http ]|
|||Monadic Decomposability of Regular Relations. Pablo Barceló, Chih-Duo Hong, Xuan Bach Le, Anthony W. Lin, and Reino Niskanen. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece. [ DOI | arXiv | http ]|
|||Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols). Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, and Philipp Rümmer. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. [ DOI | arXiv | http ]|
|||Matthew Hague, Anthony W. Lin, and Chih-Duo Hong. CSS minification via constraint solving. ACM Trans. Program. Lang. Syst., 41(2):12:1--12:76, 2019. [ DOI | http ]|
|||Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang., 3(POPL):49:1--49:30, 2019. [ DOI | http ]|
This file was generated by bibtex2html 1.99.