whispertzx

汇报内容 对于论文Extending urban Multi-lane Spatial logic to Formalise Road Junction Rules，首先该论文是对自己前序工作UMLSL的拓展，将时空结合，在她的论文中，利用^和并列的算子形式化的表示了空间的概念，并将静态信息进行了覆盖，其中将行人也视为静态信息。其中交通快照TS是通过时间和申请资源进行更新的。第二周我就上周讨论的内容进行了思考，想引入一个新的表示空间的算子，主要是想表示横着的一个概念，首先我们可以将所有的道路进行抽象表示，其中交叉路口可以用点进行描述，如下图所示。 导师反馈内容 其实可以将道路的连接算子表示为——o——>和——o「->上->下」以及「->上->下」0——这三种，但是我们如何进行拓展连接，这是可以考虑的，同时你需要认真学习空间逻辑的一些概念，并对那篇论文进行更深入的理解。

我们研一的十一月 ​   我和她，十一月的首张是猫，当早上的你看到一只喵喵，迎着阳光后，不屑的撇开了头。   我和她，在闲暇的中午后，我寻求一只粘人又甜的鹿，并将与你会面！   我和她，发现了师大无限彩虹🌈的地方，每天——见到后由于彩虹一样五彩缤纷。   我和她，在彩虹🌈的一天了，发现了征服(花卷)王，并久しぶりです吃寿喜烧。   我和她，我突然一天就成了理发大师，可是我好像已经和猫一样驼背了╥﹏╥   我和她，可能每月都会有好多次好漂亮的云吧☁️～～   我和她，在傍晚时刻发现了和太阳🌞一样的月亮🌛   我和她，一起在早上被橘猫发现了！   我和她，十一月的生活在爱乐之城下划下了暂停的休止符🎵(肯定又有好看的云☁️了呀) ...

汇报内容Reo的ppt汇报，ppt附在文章末端。 Verification of Fair Controllers for Urban Traffic Manoeuvres at Intersections论文主讲两部分，一个是交叉控制器{进行广播，将申请的资源给予给其他车，其中其他车并不理会较自己远的范围的车辆信息，对比优先级，返回no信息等}，另一个是辅助控制器，引入了优先级的概念（若被拒绝了，则增加优先级） 导师反馈内容 Reo的规范化模块化能否做？怎么做？如何描述车道间车辆转向之类的？(下周看什么？忘了。。。。)

汇报内容汇报Reo的基本操作等。 导师反馈内容 下周对Reo做一个PPT，分析Reo是什么，用来解决什么问题，举出一些例子，并讲述出Reo的语义，描述connector连接之间的性质，以及现在的编码工具、与工业界相应用的例子「产品」，它的标准，分析是否具有相应的使用价值。

汇报内容1、上周老师说了可以看看法国的BIP，然后我看了一篇关于BIP整体框架的论文，了解了一些较为基础的知识。2、这篇论文是使用BIP框架进行设计严格的组件系统，由于缺乏从一个给定系统的应用软件和平台模型中能严格推导出全局模型的技术，因此作者使用了BIP框架进行构造。3、它主要是用来保证系统的基本属性（因为现在都是对一个特定的编程模型给一个指定的执行模型进行相关联），并设计了这样一个通用的表示框架。4、例如实时一般用周期任务调度、同步用单处理顺序实现，这些都没有一定的通用性，5、而BIP统一语义模型能确保基本系统设计的正确性。6、BIP是指 behavior、interaction、priority，主要分为三块内容，一个是model-based，根据单一语义模型保证n+1步的性质满足n步的性质，一个是compoent-based，提供一系列操作符（一元和二元）、还有一个是tractable，通过构造避免单一的后验。总的来说，它的大致分为几块内容，7、定义了一个Architecture，8、包含原子组件（仅有interaction和priortes构成）和复杂组件（原子+原子或者原子 ...

汇报内容1、汇报formalmethod一书的第五章以及论文Scheduling Games for Concurrent Systems ​ 论文：进程之间分配处理，调度引入了依赖，产生了延迟。将工作自动机和并行程序的调度问题看作调度程序与工作自动机的博弈。Game表示图形上的符号玩法，由工作自动机和并行及其推导，game每一次玩法，对应工作自动机run一次=>推出游戏策略对应调度策略在工作自动机(发现最小化上下文切换数量的调度)。调度策略并不完全决定并发执行顺序。 ​ 提出两个东西：一个是工作自动机，另一个是mean payoff games平均收益博弈论 ​ 「时间自动机 –> 工作自动机 ​ 时钟约束 –> 扩展了带工作约束 ​ 时钟估值 –> 作业约束 ...

我们研一的十月   我和她十月的吃喝玩乐行动开始啦，国庆第一天就去吃Pier 39！🐷🐷🐷   我和她国庆的第二天当然还是休息啦～～～，去了长风公园，恰了城市麻辣烫，还有罗森的冰皮月亮蛋糕！   我和她国庆第四天的撸猫行动！都是同类生物，猫猫🐱就主动过来啦～   国庆第五天，我回到吃食堂菜的正常生活去（主要是她去找麻麻了）。   在风和日丽的一天，她定义了标准云☁️，我也着迷其中，拍了很多。   没错！过了几天，我和她还在拍标准云☁️～   我和她报名了学校七十周年校庆的观众，白嫖帅气的白色卫衣。   十月的运动会赐予了我和她去迪士尼的机会，然而我们的抽奖运气不是很好哈哈哈😄   我与她涌入迪士尼白天的花车游行和晚上万圣节的花车游 ...

汇报内容1、汇报formal method一书的第三章 ​ 第三章中的的一个问题，用不变量(invariants)在不同点进行检查程序的正确性，什么意思？ ​ 第三章讲述了什么是程序验证，什么是谓词，表达程序正确需要引入足够的符号等 ​ 导师反馈内容 1、《面向智能驾驶的多粒度动态认知决策行为建模与验证方法》一个项目中，从三个方向进行保证自动驾驶，时空理论、精化理论(粒度粗细)、协同方法进行思考。 精化理论：粗细粒度、如何决策、如何预测（后面两个不一定属于精化理论） 其中对于多种粒度之间划分，其中粗粒度是对于决策不紧急且决策快，细粒度是需要紧急处理且时间长，但细粒度得包含在粗粒度中，这里有一个问题，即如何对于多种粒度之间的一致性如何保证(精化理论)。 接着example车辆行驶： 粗粒度：后面车的去向进行划分区域，且区域距离我方左转还远或者我方车并不会左转(即划定不能去的范围) 细粒度：决策出后方车所有的决策路线，且出现我方车左转，且对方车也会出现这条路上 更细粒度：预测对方轨道的权重分配，作出最有可能的决策 2、什么是不变式，不变式存在的情况 1 ...

汇报内容1、汇报论文《Predicate Abstraction for Program Verification Safety and Termination》 ​ 本周阅读了对于程序验证的安全性和终止性的谓词抽象，论文表达了程序正确性属性包含两种：safety安全性（即错误状态不可达）和termination终止。引入两个概念，谓词抽象和反例引导抽象精化，我认为这个与上次老师讲述的refinement相关。论文首先介绍了一个类似的状态迁移系统，引入了V、PC、字母表等符号，其中Φ表达可达的状态集合，pesai表达可达的状态对，其中论文指出安全性可以用状态的可达描述，终止性可以用状态对的可达进行描述。 ​ 即程序安全Φreach=字母表/Φerr，其中Φreach是通过有限次迭代进行构造。接着引入程序P是可终止的，即当析取n个well-founded关系是转移不变量，Ψreach。。。Ψ1.。。Ψ2.。。Ψn，其中用有限数目的有充分的基础关系的并构成转移不变量，其中这个是事实，依赖于拉姆齐定理。然后论文通过归纳的方法来描述正确性，引入post后置函数，函数 ...

Week1 常见的基本句型： ​ 1、简单句：主+谓+(宾+宾补) ​ 2、并列句：简单句，+并列连词，+简单句。常用的并列连词有for、and、nor、but等 ​ 3、复合句：复合句由一个独立分句和一个或一个以上的从句构成（定语从句、状语从句、名词性从句） ​ 4、并列复合句：并列复合句由两个独立分句及一个或一个以上的从句构成 Week2 如何将文章词汇变得高级： ​ 1、名词化 ​ 2、非谓语 -ed -ing ​ 3、前缀和后缀表达 ​ 4、熟练的使用连接词 ​ 5、复合词的使用：take-off Week3 文章中存在的句式问题： ​ 1、缺少成分：sentences fragments ​ 2、过多简单句：choppy sentences ​ 3、符号错误(, . ;)，独立句子和非独立句子之间：Run-on sentences and comma splices ​ 4、串联句问题，句子 ...