Games for Good
Lead Research Organisation:
University of Liverpool
Department Name: Computer Science
Abstract
"It is easy to be wise after the event." -- Arthur Conan Doyle.
Making an optimal decision it is ever so much easier with hindsight. This is true in our daily life - wouldn't it be great to be able to fill in the bet for the national lottery after the draw took place? - but it also holds true in the analysis of computational systems. What makes hindsight so attractive is, naturally, the full knowledge of the future, and it is similarly clear that we do not always possess this knowledge at the point where it would be really useful to have it.
The principle research question in this project is the question whether we can make just as good a decision without hindsight as we can do with it.
While this is clearly not the case for filling in the lottery slip, there are other decisions that can be made without having to know the future.
In formal verification, this is a very desirable property, because it allows us to make decisions on the fly, and without regret: we do not have to see what the future holds, but can make optimal decisions on the past. But which specification has this property? And what is the cost to turn a specification that does not possess this property into one that does?
These are deep questions that have been studied for finite state systems, where it is possible to translate a language acceptor into an equivalent one that just does not need hindsight (but is not necessarily deterministic).
Such a translation is always possible for a wide class of quantitative specification languages, simply because their acceptors (finite or omega automata) can be determinized, albeit at very high cost.
Removing hindsight is a little bit simpler than determinization (removing all choice), and this little advantage can make a huge difference, so that it recently became a very active and insightful branch of verification.
This project will solve the questions that arise when the systems and specification languages do not have finite representations. Here, waiving hindsight is not just more efficient and concise than determinizing, it is also more expressive. We will find out just how much more expressive in which context, and just how much more concise. This will allow for follow-up research that accelerates the verification and validation of real-world systems, ultimately making them safer and more reliable.
Making an optimal decision it is ever so much easier with hindsight. This is true in our daily life - wouldn't it be great to be able to fill in the bet for the national lottery after the draw took place? - but it also holds true in the analysis of computational systems. What makes hindsight so attractive is, naturally, the full knowledge of the future, and it is similarly clear that we do not always possess this knowledge at the point where it would be really useful to have it.
The principle research question in this project is the question whether we can make just as good a decision without hindsight as we can do with it.
While this is clearly not the case for filling in the lottery slip, there are other decisions that can be made without having to know the future.
In formal verification, this is a very desirable property, because it allows us to make decisions on the fly, and without regret: we do not have to see what the future holds, but can make optimal decisions on the past. But which specification has this property? And what is the cost to turn a specification that does not possess this property into one that does?
These are deep questions that have been studied for finite state systems, where it is possible to translate a language acceptor into an equivalent one that just does not need hindsight (but is not necessarily deterministic).
Such a translation is always possible for a wide class of quantitative specification languages, simply because their acceptors (finite or omega automata) can be determinized, albeit at very high cost.
Removing hindsight is a little bit simpler than determinization (removing all choice), and this little advantage can make a huge difference, so that it recently became a very active and insightful branch of verification.
This project will solve the questions that arise when the systems and specification languages do not have finite representations. Here, waiving hindsight is not just more efficient and concise than determinizing, it is also more expressive. We will find out just how much more expressive in which context, and just how much more concise. This will allow for follow-up research that accelerates the verification and validation of real-world systems, ultimately making them safer and more reliable.
