Report

Teaser, summary, work performed and final results

Periodic Reporting for period 3 - AVS-ISS (Analysis, Verification, and Synthesis for Infinite-State Systems)

Teaser

The main focuses of this project is on theoretical problems arising out of automated-verification research, broadly construed, with a particular emphasis on algorithmic questions. During the reporting period, our efforts have revolved around the analysis of discrete and...

Summary

The main focuses of this project is on theoretical problems arising out of automated-verification research, broadly construed, with a particular emphasis on algorithmic questions. During the reporting period, our efforts have revolved around the analysis of discrete and continuous linear dynamical systems. Such systems are widely used as abstractions of components of computer programs and embedded systems, including cyber-physical systems, that are ubiquitous in our modern society. The problems considered include reachability, invariant synthesis, performance, and controllability questions -- such questions relate intimately to the correct and dependable workings of many of the computer systems around us.

The overall objective is to comprehensively map the algorithmic landscape of verification problems for both discrete and continuous linear dynamical systems, and attendant extensions.

Work performed

During the reporting period, we mainly tackled fundamental scientific questions relating to reachability and invariant generation for linear dynamical systems. Our main results are the following:

1) The solution of a 30-year old problem of Kannan and Lipton, published in our JACM 2016 paper.

2) The solution of the hyperplane-hitting problem for continuous linear dynamical systems (or equivalently the zero problem for linear differential equations), subject to Schanuel\'s Conjecture, as published in our LICS 2016 and ICALP 2016 papers.

3) An algorithm for to decide the existence of, and synthesise, semialgebraic invariants for discrete-time linear dynamical systems, for the point-to-point reachability problem, published in a STACS 2017 paper. We were subsequently invited to submit an extended
version of this work to the journal Theory of Computing Systems, and our paper has been accepted subject to minor corrections.

4) The decidability of the longstanding question of structural liveness for linear hybrid systems is decidable, published in out HSCC 2017 paper.

Final results

A major thrust of our ongoing research agenda is in the area of automated invariant synthesis. Invariants are one of the most fundamental and useful notions in the quantitative sciences, and within computer science play a central role in areas such as program analysis and verification, abstract interpretation, static analysis, and theorem proving. To this day, automated invariant synthesis remains a topic of active research. In program analysis, invariants play a central role in methods and tools seeking to establish correctness properties of computer programs, including -- but not limited to -- termination analysis. We expect to provide algorithmic techniques for the automatic synthesis of invariants, answering questions that have been open for several years.

We are expecting some major advances in the area of automated invariant synthesis by the end of the project.