|
| EPSRC Reference: |
EP/F036361/1 |
| Title: |
Game semantics, recursion schemes and collapsible pushdown automata: a new approach to the algorithmics of infinite structures |
| Principal Investigator: |
Professor CHL Ong |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Computing Laboratory |
| Organisation: |
University of Oxford |
| Scheme: |
Standard Research |
| Starts: |
15 July 2008 |
Ends: |
14 October 2012 |
Value (£): |
522,778
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
06 Dec 2007
|
ICT Prioritisation Panel (Technology)
|
Announced
|
|
|
Summary |
Despite considerable progress over the past decade, the computer-aided verification of software remains a hugely challenging problem. There are two main reasons. First, programs are infinite-state systems, but verification tools of industrial scale are essentially finite-state technologies. Secondly, modern programs -- in which unbounded data types, complex memory operations, non-local control flow, higher-order constructs, and name bindings of various kinds etc. are key features -- can only be accurately modelled using highly-structured mathematical models, as studied in semantics. Relatively little is known about the algorithmic properties of such rich, often "higher-order'', mathematical structures.
This project concerns an approach to software verification by developing automatic techniques which deal directly with infinite-state systems that are highly accurate models of programs. Striking examples of such infinite-state models are fully abstract game semantics of higher-order procedural programs; these models can be represented as (variant classes of higher-order) pushdown automata.
In recent years, there have been remarkable advances in the study of algorithmic properties of hierarchies of generically-defined infinite structures. A notable result is that ranked trees that are generated by higher-order recursion schemes have decidable monadic second-order theories (Ong LICS'06). Further there is a new variant hierarchy of higher-order pushdown automata, called collapsible pushdown automata, that are equi-expressive with higher-order recursion schemes (in the sense that they generate the same class of trees), subsuming well-known structures at low orders: trees at order 0 and 1 are respectively the regular (Rabin 1969) and algebraic (Courcelle 1995) trees. The discovery of this rich, unifying and robust hierarchy of trees with excellent model-checking properties sparked the present research proposal.
We have two general goals:
- First we plan to study the connexions between the two closely-related higher-order families of generators (i.e. recursion schemes and collapsible pushdown automata), to explore the logical-algorithmic theory of infinite structures generated by them, and to derive (local and global) model checking algorithms.
- Secondly we aim to develop verification techniques and construct efficient implementations of symbolic model-chekcers of reachability and temporal logics for these infinite structures of low orders.
Why is it important to pursue these goals?
- First, these hierarchies of infinite structures lie at the very frontier of infinite-state verification. The family of ranked trees thus generated is, to date, the largest generically-defined family of trees known to have decidable monadic second-order (MSO) theories; the family of transition graphs thus generated (does not have decidable MSO theories but) is, to date, the largest that is known to have decidable modal mu-calculus theories. These are significant indicators of our understanding of the subject, as MSO logic is the gold standard of languages for describing model-checking properties in computer-aided verification.
- Secondly, these hierarchies of infinite structures are (representations of) highly accurate models of computation for higher-order procedural programs (such as OCAML, Haskell and F#). Recent results in (algorithmic) game semantics have shown that they underpin the computer-aided verification of these programs, an important and challenging direction for the next generation of software model checkers.
|
| Final Report Summary |
|
No final report summary is available for this grant.
|
| Further Information: |
|
| Organisation Website: |
http://www.ox.ac.uk |
|
|