Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. In this paper we provide proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint. The theory is developed for non-expansive monotone functions on suitable lattices of the form $\mathbb{M}^Y$, where $Y$ is a finite set and $\mathbb{M}$ an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, behavioural distances for probabilistic automata and bisimilarity. Moreover, quite interestingly, it allows us to determine original algorithms for solving simple stochastic games.


翻译:Knaster- Tarski 的定理, 将一个单调函数的最大固定点描述为一个完整的固定点上的最大固定点, 作为最大的后定点, 自然导致所谓的点数证明原则, 以显示某些元素低于最大固定点( 例如, 提供两个相似的证人 ) 。 用于显示一个元素高于最小固定点的双重原则 与诱导性变量有关。 在本文中, 我们提供了在精神上相似但显示一个元素高于最大固定点或双倍低于最小固定点的校正规则 。 该理论是针对表格$\ mathb{ M ⁇ Y$( 提供两个不同的证人 ) 的合适固定点上的非扩展单调单调函数制定的。 该理论是用来显示一个元素低于最大固定点( $Y) 和 $\ mathb{ M} 用于显示一个最小固定点的元素的双重原则 。 它基于最初功能的构造。 我们显示, 我们的理论适用于一系列的例子, 包括终止性概率、 行为距离, 使原始的游戏能够进行原始的自动解算算。

0
下载
关闭预览

相关内容

迄今为止,产品设计师最友好的交互动画软件。

专知会员服务
52+阅读 · 2020年9月7日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
2019年机器学习框架回顾
专知会员服务
35+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
已删除
将门创投
7+阅读 · 2020年3月13日
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
RL 真经
CreateAMind
5+阅读 · 2018年12月28日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
[DLdigest-8] 每日一道算法
深度学习每日摘要
4+阅读 · 2017年11月2日
Arxiv
0+阅读 · 2021年3月15日
Arxiv
0+阅读 · 2021年3月15日
VIP会员
相关VIP内容
专知会员服务
52+阅读 · 2020年9月7日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
2019年机器学习框架回顾
专知会员服务
35+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
相关资讯
已删除
将门创投
7+阅读 · 2020年3月13日
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
RL 真经
CreateAMind
5+阅读 · 2018年12月28日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
[DLdigest-8] 每日一道算法
深度学习每日摘要
4+阅读 · 2017年11月2日
Top
微信扫码咨询专知VIP会员