新书推介：《语义网技术体系》
作者：瞿裕忠，胡伟，程龚
   XML论坛     W3CHINA.ORG讨论区     计算机科学论坛     SOAChina论坛     Blog     开放翻译计划     新浪微博  
 
  • 首页
  • 登录
  • 注册
  • 软件下载
  • 资料下载
  • 核心成员
  • 帮助
    		•   Add to Google

    >> It is the theory that decides what can be observed. - Albert Einstein
    [返回] 计算机科学论坛 → 计算机理论与工程 → 『 理论计算机科学 』 → 这里有没有做Model Checking的？ ◇查看新帖 ◇ 用户列表 ◇

      发表一个新主题  发表一个新投票  回复主题  (订阅本版) 您是本帖的第 42954 个阅读者浏览上一篇主题  刷新本主题   树形显示贴子　浏览下一篇主题
     * 贴子主题： 这里有没有做Model Checking的？ 举报  打印  推荐  IE收藏夹 
       本主题类别:     
     ljb 帅哥哟，离线，有人找我吗？
      
      
      等级：大二(研究C++)
      文章：39
      积分：271
      门派：XML.ORG.CN
      注册：2005/3/19

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给ljb发送一个短消息 把ljb加入好友 查看ljb的个人资料 搜索ljb在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看ljb的博客第11楼
    发贴心情 

    “尤其是在使用自动机来识别图时。” 这个东西哪里有介绍？？

    以下是引用yangfeather在2005-4-5 0:33:10的发言：
    关于model checking:
      1. 在模型检测中，我们关注的往往是local property，而不是global property，所以使用时序逻辑，模态mu演算等等，而不是使用一阶逻辑或者二阶逻辑，当然前者与后者有一定的关系，具体的关系，可以学习一下关于modal logic的一些知识，在modal logic的框架内看这些问题，就能很清晰。
    2. 在model checking中，还是有很多的理论问题可以做的，比如LTL的模型检测中，Buchi自动机的求补问题，如何提高效率；modal mu calculus中多个不动点嵌套的公式的模型检测问题；时序逻辑，modal mu caluclus的描述能力的问题，这些问题都是非常难得，说实在的，就国内研究的水平来说，做这些问题，还是比较困难的，风险也比较大(弄不好，就毕不了业）。
    3.在model checking的理论研究中，尤其是在研究逻辑的描述能力的问题中，自动机是一个比较主要的工具，game theory也有被运用，尤其是在使用自动机来识别图时。
                                                                  


    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/4/5 9:19:00
     
     copperccnu 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：6
      积分：84
      门派：XML.ORG.CN
      注册：2005/3/12

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给copperccnu发送一个短消息 把copperccnu加入好友 查看copperccnu的个人资料 搜索copperccnu在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看copperccnu的博客第12楼
    发贴心情 
    武大的同学，书不在我手上，不好意思啊。网上可以找到一些论文，CMU有几个TR可以下载来看，都是以前的PhD Thesis。

    最近在看将LTL公式转换成Buchi自动机后如何约简自动机提高效率的文章。yangfeather，你提到的Buchi自动机求补问题，的确还没有认真想过。

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/4/5 20:05:00
     
     zhaoming 帅哥哟，离线，有人找我吗？
      
      
      等级：大二期末(数据结构考了98分!)
      文章：50
      积分：360
      门派：XML.ORG.CN
      注册：2005/4/22

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给zhaoming发送一个短消息 把zhaoming加入好友 查看zhaoming的个人资料 搜索zhaoming在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看zhaoming的博客第13楼
    发贴心情 
    以前看到一本书<model checking>,翻了一下,挺好,没细看,
    在做automata,涉及到TCTL和STCTL,觉得这方面面太广,一个人能做的太有限,
    可选的题目太多太多.
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/4/22 19:00:00
     
     twosteps 美女呀，离线，快来找我吧！
      
      
      等级：大一新生
      文章：4
      积分：68
      门派：XML.ORG.CN
      注册：2005/8/1

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给twosteps发送一个短消息 把twosteps加入好友 查看twosteps的个人资料 搜索twosteps在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看twosteps的博客第14楼
    发贴心情 
    举个小手， 偶的毕业论文大方向就是这个， 我是在国外念的大学，很想以后回国工作，不过今天浏览了这个论坛后，发现很多专业词中文都不知道，只能马马乎乎的瞎猜。。。以后还要多请教各位大侠。
    上面提到的那个 buchi automaton 求 complement 的问题，印象中是要分情况讨论的，也就是 deterministic 和 nondeterministic， 因为 deterministic buchi automata 比较 weak, 而nondeterministic buchi automata 和 muller, rabin, parity 是equivalent 的。也可能说的不对，以前学的，考完就忘了。。。
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/8/1 8:59:00
     
     twosteps 美女呀，离线，快来找我吧！
      
      
      等级：大一新生
      文章：4
      积分：68
      门派：XML.ORG.CN
      注册：2005/8/1

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给twosteps发送一个短消息 把twosteps加入好友 查看twosteps的个人资料 搜索twosteps在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看twosteps的博客第15楼
    发贴心情 
    偶以前学过自动机识别二维图，实际上识别的就是识别一个数组。不知道是不是你想问的。
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/8/1 9:04:00
     
     fq4731 美女呀，离线，快来找我吧！
      
      
      等级：大一(猛啃高等数学)
      文章：24
      积分：142
      门派：XML.ORG.CN
      注册：2004/7/16

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给fq4731发送一个短消息 把fq4731加入好友 查看fq4731的个人资料 搜索fq4731在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看fq4731的博客第16楼
    发贴心情 
    有研究进程代数和pi演算进行模型验证的吗？
    有的话可以讨论讨论哦
    QQ：361169937
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/8/12 15:25:00
     
     skatingon 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：1
      积分：58
      门派：XML.ORG.CN
      注册：2005/8/14

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给skatingon发送一个短消息 把skatingon加入好友 查看skatingon的个人资料 搜索skatingon在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看skatingon的博客第17楼
    发贴心情 
    我在做Isabelle/Isar，有没有同学也做这个？skatingon@gmail.com
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/8/14 20:40:00
     
     royzy 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：1
      积分：60
      门派：XML.ORG.CN
      注册：2005/8/25

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给royzy发送一个短消息 把royzy加入好友 查看royzy的个人资料 搜索royzy在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看royzy的博客第18楼
    发贴心情 
    偶今年刚上研一，对这个形式化验证的东西不太了解，我想请教一些问题，如果要把这个模型检测和实际的东西结合起来的话，除了Spin.STeP这样的东西外，还能从哪方面着手呀？？
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/8/25 15:10:00
     
     hgawu 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：0
      积分：58
      门派：XML.ORG.CN
      注册：2005/10/7

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给hgawu发送一个短消息 把hgawu加入好友 查看hgawu的个人资料 搜索hgawu在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看hgawu的博客第19楼
    发贴心情 
    这位老兄说的好，不知道是何方神圣？我也是做进程代数的。交流交流如何？
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2006/3/25 17:11:00
     
     sosoid 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：3
      积分：64
      门派：XML.ORG.CN
      注册：2006/3/30

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给sosoid发送一个短消息 把sosoid加入好友 查看sosoid的个人资料 搜索sosoid在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看sosoid的博客第20楼
    发贴心情 
    瞎逛逛到这里了
    原来有这么多人做model checking的
    我刚上研 这些方面刚看了两本书

    1

    面向计算机科学的数理逻辑（影印，不是陆老师那本）
    Logic in Computer Science
    Modelling and Reasoning about Systems
    2nd Edition
    （这本对逻辑方面讲了很多，模态逻辑等等）
    http://www.cambridge.org/catalogue/catalogue.asp?isbn=052154310X

    2
    SPIN model checker（粗略看完）

    3
    model checking（ 借了还没翻呢 呵呵）

    以后来这边和大家多交流 呵呵

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2006/3/30 9:48:00
     
     GoogleAdSense
      
      
      等级：大一新生
      文章：1
      积分：50
      门派：无门无派
      院校：未填写
      注册：2007-01-01
    给Google AdSense发送一个短消息 把Google AdSense加入好友 查看Google AdSense的个人资料 搜索Google AdSense在『 理论计算机科学 』的所有贴子 访问Google AdSense的主页 引用回复这个贴子 回复这个贴子 查看Google AdSense的博客广告
    2024/5/15 13:31:32

    本主题贴数24，分页： [1] [2] [3]

    管理选项： 修改tag | 锁定 | 解锁 | 提升 | 删除 | 移动 | 固顶 | 总固顶 | 奖励 | 惩罚 | 发布公告
    W3C Contributing Supporter! W 3 C h i n a ( since 2003 ) 旗 下 站 点
    苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
    		 109.375ms