Games for Good

“事后聪明很容易。“--亚瑟柯南道尔。事后诸葛亮，做最佳决定要容易得多。这在我们的日常生活中是真实的-如果能够在开奖后为国家彩票投注，那不是很好吗？- 但它也适用于计算系统的分析。后见之明之所以如此有吸引力，自然是因为它对未来有充分的了解，同样清楚的是，我们并不总是在拥有这些知识会真正有用的时候拥有这些知识。这个项目的主要研究问题是，我们是否可以在没有后见之明的情况下做出和我们可以做的一样好的决定。虽然这显然不是填写彩票单的情况，在形式验证中，这是一个非常理想的属性，因为它允许我们在飞行中做出决定，并且没有遗憾：我们不必看到未来会发生什么，但可以根据过去做出最佳决策。但是，哪种规格说明具有这种性质呢？把一个不具备这种属性的规范变成一个具备这种属性的规范的成本是多少？这些都是有限状态系统研究过的深层次问题。在有限状态系统中，可以将语言接受器转换为等价的语言接受器，而不需要事后诸葛亮（但不一定是确定性的）。这样的转换对于大量的定量规格说明语言来说总是可能的，仅仅因为它们的接受器（有限自动机或欧米茄自动机）可以确定，尽管代价很高。去除后见之明比确定性（去除所有选择）简单一点，这个小小的优势可以产生巨大的差异，因此它最近成为验证的一个非常活跃和有见地的分支。这个项目将解决当系统和规范语言没有有限表示时出现的问题。在这里，放弃事后诸葛亮不仅比确定性更有效、更简洁，而且也更有表现力。我们会发现在什么样的语境下表达能力会更强，表达能力会更简洁。这将允许后续研究，加速真实世界系统的验证和确认，最终使其更安全，更可靠。

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