Games for Good

“事后诸葛亮是很容易的。”--阿瑟·柯南·道尔。事后看来，做一个最优的决定比以往任何时候都要容易得多。这在我们的日常生活中是正确的--能够在抽奖后填写国家彩票的赌注不是很棒吗？--但在计算机系统分析中也是如此。后见之明之所以如此有吸引力，自然是因为我们对未来有充分的了解，同样清楚的是，我们并不总是在拥有这些知识的时候拥有这些知识。这个项目的主要研究问题是，我们是否可以在没有后见之明的情况下做出和我们可以做的一样好的决定。虽然这显然不是填写彩票的情况，但还有其他决定可以在不知道未来的情况下做出。在正式验证中，这是一个非常可取的属性，因为它允许我们在飞行中做出决定，而不会后悔：我们不必看到未来会发生什么，但可以对过去做出最佳决定。但是哪种规格有这个属性呢？把不具备这种性质的规格说明转换成具有这种性质的规格说明的代价是什么？这些都是有限状态系统中研究过的深层次问题，在有限状态系统中，将语言接受者翻译成等价的语言接受者是可能的，不需要事后诸葛亮(但不一定是确定性的)。这样的翻译对于一大类量化规范语言总是可能的，只是因为它们的接受者(有限或omega自动机)可以确定，尽管成本非常高。删除后见之明比确定化(删除所有选项)要简单一点，这个小小的优势可以产生巨大的差异，因此它最近成为了一个非常活跃和有洞察力的验证分支。这个项目将解决当系统和规范语言没有有限表示时出现的问题。在这里，放弃后见之明不仅比确定更高效、更简洁，而且更有表现力。我们将找出在哪种背景下的表现力要强多少，以及要简明得多。这将允许进行后续研究，加快对现实世界系统的验证和确认，最终使它们更安全、更可靠。

"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.