Official versions can be found under the DOI reference while extended technical reports are available as an arXiv/.pdf link.
Learning Union of Integer Hypercubes with Queries (with applications to
Oliver Markgraf, Daniel Stan, and Anthony Widjaja Lin.
In CAV 2021 (to appear).
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 modulos 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 Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, 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 Dang Van Hung and Oleg Sokolsky, editors, 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 Bruno C. d. S. Oliveira, editor, 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 Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 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 Isil Dillig and Serdar Tasiran, editors, 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.