Counter Automata: Verification and Synthesis
Lead Research Organisation:
University of Warwick
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
Publications
Blondin M
(2021)
The Reachability Problem for Two-Dimensional Vector Addition Systems with States
in Journal of the ACM
Chattopadhyay A
(2021)
Pumping lemmas for weighted automata
in Logical Methods in Computer Science
Chattopadhyay A
(2020)
Pumping lemmas for weighted automata
Clemente L
(2017)
Timed pushdown automata and branching vector addition systems
Clemente L
(2019)
Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems
in ACM Transactions on Computational Logic
Colcombet T
(2017)
Perfect half space games
Englert M
(2021)
A lower bound for the coverability problem in acyclic pushdown VAS
in Information Processing Letters
Figueira D.
(2017)
Polynomial-space completeness of reachability for succinct branching VASS in dimension one
in Leibniz International Proceedings in Informatics, LIPIcs
| Description | Our first achievement was to determine exactly how much computational time and space is needed to determine the winner in large games between two players who repeatedly take turns and produce or consume resources across several dimensions. This fundamental question had resisted attempts by the international research community for over five years prior to our 2015 paper at the prestigious ICALP 2015 conference. Subsequently, these results have been communicated at conferences and seminars at Bellairs, Bordeaux, IIT Delhi, Evry, Paris 7, Prague, Queen Mary UL, Reykjavik and Warsaw, and applied to verification of multi-agent systems (Alechina et al., RP 2016) and to population control in computational biology (Bertrand et al., CONCUR 2017). Our second major achievement was to discover a surprisingly efficient algorithm for verifying safety of two-dimensional vector addition systems, which are ubiquitous models of concurrent processes and have extensive applications in verification of software. The algorithm is based on novel structural insights, that provided the basis for the current Leverhulme Trust Research Fellowship (10/2017-12/2018) awarded to Lazic (PI of this award). Our third group of achievements were determining the computational resources required for the analysis of one-dimensional branching vector addition systems. With collaborators at the University, we then succeeded in leveraging those results and our associated newly developed techniques to discover an algorithm for verifying software systems that feature recursive programming as well as operate in critical real-time environments, published at the top LICS 2017 conference. Our fourth line of research has led to a powerful unifying understand of verifying safety of a wide range of systems with unbounded features, which we then used to determine the computational time and space requirements for verifying massively concurrent systems that operate on unbounded data. The latter work, published at LICS 2016, has highlighed a novel high-complexity class ('double Ackermannian') and has produced techniques that other leading researches have already applied successfully to distinct problems (Benedikt et al., LICS 2017). |
| Exploitation Route | Our findings have already been applied and extended in unexpected ways by other researchers in the field, and several such instances are indicated above. We believe that our ground-braking work on two-dimensional vector addition systems has potential to lead to a solution on the long-standing open problem of efficiently verifying general vector addition systems, that has been open since the 1970s and has eluded attempts even by Turing Award winners (the equivalent in computer sciece of the Nobel Prize). As a whole, the findings of this grant constitute substantial advances in the theory of formal verification. We therefore expect that, in the short to medium term, they will enable development of a new generation of verification tools that are able to handle highly concurrent systems that process massive quantities of data, branching from academic prototypes to industrial deployments. Corresponding academic applied work has already taken place: our findings have influenced the currently state-of-the-art safety verifiers QCover (Blondin et al., TACAS 2016) and ICover (Geffroy et al., SPIN 2017). |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | Research Fellowship |
| Amount | £48,106 (GBP) |
| Organisation | The Leverhulme Trust |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 10/2017 |
| End | 12/2018 |