具有负面和定量前提的概率转换系统规范中的树规则
摘要：概率转换系统规范（PTSS）以ntmufnu/ntmuxnu格式为Segala类型的系统提供结构性操作语义，该系统同时表现出概率和非确定性行为，并保证了isimilarity是一个同构。与tyft/tyxt规则格式的非确定性情况类似，我们表明在概率设置中无需满足基础性要求。为了实现这一点，我们首先定义了ntmufnu/ntmuxnu格式的扩展版本，其中定量前提和结论包括分布的嵌套凸组合。该格式还保证了同步性是一个同构。然后，对于给定的（可能非基础的）新格式PTSS，我们构建了一个等效的基础转换系统，该系统只包含较简单（基础）概率ntree格式的规则。此外，我们针对这些PTSS开发了一个证明理论概念，如果PTSS是可分层的，那么它与现有的基于分层的含义相一致。这继续了将结构性操作语义结果从非确定性设置提升到具有概率和非确定性行为的系统的研究。
作者：Matias David Lee (Famaf, UNC - Conicet), Daniel Gebler (VU University Amsterdam), Pedro R. D'Argenio (Famaf, UNC - Conicet)
论文ID：1208.2752
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-08-15